File tree Expand file tree Collapse file tree 2 files changed +2
-2
lines changed
Expand file tree Collapse file tree 2 files changed +2
-2
lines changed Original file line number Diff line number Diff line change @@ -92,7 +92,7 @@ let locate_constant r =
9292 try
9393 let gr = Smartlocate. locate_global_with_alias r in
9494 match gr with
95- | Globnames .ConstRef cst -> cst
95+ | Names.GlobRef .ConstRef cst -> cst
9696 | _ -> CErrors. user_err (str " A constant is expected: " ++ Printer. pr_global gr)
9797 with Not_found -> CErrors. user_err (str " Not found: " ++ Libnames. pr_qualid r)
9898
Original file line number Diff line number Diff line change @@ -66,7 +66,7 @@ VERNAC COMMAND EXTEND CWFileNegMatch CLASSIFIED AS QUERY
6666 }
6767END
6868
69- VERNAC COMMAND EXTEND CWCompileAndRun CLASSIFIED AS SIDEFF
69+ VERNAC COMMAND EXTEND CWCompileAndRun CLASSIFIED AS QUERY
7070| [ "CWCompileAndRun" string_list(files) "Options" string_opt(options) "Driver" string(driver) ] -> {
7171 Coq_cw.compile_and_run files ?options driver
7272 }
You can’t perform that action at this time.
0 commit comments