Split Logic into subdirectories

proux01 · Sep 21, 2024 · 80ffe33 · 80ffe33
1 parent 7cd96ee
commit 80ffe33
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/library/coqlib.ml b/library/coqlib.ml
@@ -20,7 +20,7 @@ let coq = Libnames.coq_string (* "Stdlib" *)
 
 let init_dir = [ coq; "Init"]
 
-let jmeq_module_name = [coq;"Logic";"JMeq"]
+let jmeq_module_name = [coq;"Logic";"Base"; "Stdlib"; "Logic"; "JMeq"]
 
 let find_reference locstr dir s =
   let dp = make_dir dir in

diff --git a/pretyping/program.ml b/pretyping/program.ml
@@ -44,7 +44,7 @@ let mk_coq_not env sigma x =
 let coq_JMeq_ind  () =
   try Coqlib.lib_ref "core.JMeq.type"
   with Not_found ->
-    user_err (Pp.str "cannot find Stdlib.Logic.JMeq.JMeq; maybe library Stdlib.Logic.JMeq has to be required first.")
+    user_err (Pp.str "cannot find Stdlib.Logic.Base.Stdlib.Logic.JMeq.JMeq; maybe library JMeq from Stdlib has to be required first.")
 let coq_JMeq_refl () = Coqlib.lib_ref "core.JMeq.refl"
 
 (* let coq_not () = Universes.constr_of_global @@ Coqlib.lib_ref "core.not.type" *)