From 0d98057cdd6fc8ab8ae0770b8e6ab810d07c6dcf Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 10 Jul 2024 13:02:43 +0200 Subject: [PATCH] Split Logic into subdirectories --- library/coqlib.ml | 2 +- pretyping/program.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/library/coqlib.ml b/library/coqlib.ml index b85905b527ee..293b06846b2b 100644 --- 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 index a12983d31a74..c0e4cd818579 100644 --- 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" *)