diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/coqlib.ml | 12 | ||||
| -rw-r--r-- | library/global.ml | 44 | ||||
| -rw-r--r-- | library/global.mli | 10 |
3 files changed, 9 insertions, 57 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml index 677515981a..784360dc8a 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -14,7 +14,6 @@ open Pp open Names open Libnames open Globnames -open Nametab let make_dir l = DirPath.make (List.rev_map Id.of_string l) @@ -79,7 +78,7 @@ let register_ref s c = (* Generic functions to find Coq objects *) let has_suffix_in_dirs dirs ref = - let dir = dirpath (path_of_global ref) in + let dir = dirpath (Nametab.path_of_global ref) in List.exists (fun d -> is_dirpath_prefix_of d dir) dirs let gen_reference_in_modules locstr dirs s = @@ -228,8 +227,7 @@ type coq_eq_data = { (* Leibniz equality on Type *) -let build_eqdata_gen lib str = - let _ = check_required_library lib in { +let build_eqdata_gen str = { eq = lib_ref ("core." ^ str ^ ".type"); ind = lib_ref ("core." ^ str ^ ".ind"); refl = lib_ref ("core." ^ str ^ ".refl"); @@ -238,9 +236,9 @@ let build_eqdata_gen lib str = congr = lib_ref ("core." ^ str ^ ".congr"); } -let build_coq_eq_data () = build_eqdata_gen logic_module_name "eq" -let build_coq_jmeq_data () = build_eqdata_gen jmeq_module_name "JMeq" -let build_coq_identity_data () = build_eqdata_gen datatypes_module_name "identity" +let build_coq_eq_data () = build_eqdata_gen "eq" +let build_coq_jmeq_data () = build_eqdata_gen "JMeq" +let build_coq_identity_data () = build_eqdata_gen "identity" (* Inversion data... *) diff --git a/library/global.ml b/library/global.ml index 1ad72afea1..3781ff3230 100644 --- a/library/global.ml +++ b/library/global.ml @@ -167,48 +167,8 @@ let env_of_context hyps = open Globnames -(** Build a fresh instance for a given context, its associated substitution and - the instantiated constraints. *) - -let constr_of_global_in_context env r = - let open Constr in - match r with - | VarRef id -> mkVar id, Univ.AUContext.empty - | ConstRef c -> - let cb = Environ.lookup_constant c env in - let univs = Declareops.constant_polymorphic_context cb in - mkConstU (c, Univ.make_abstract_instance univs), univs - | IndRef ind -> - let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - let univs = Declareops.inductive_polymorphic_context mib in - mkIndU (ind, Univ.make_abstract_instance univs), univs - | ConstructRef cstr -> - let (mib,oib as specif) = - Inductive.lookup_mind_specif env (inductive_of_constructor cstr) - in - let univs = Declareops.inductive_polymorphic_context mib in - mkConstructU (cstr, Univ.make_abstract_instance univs), univs - -let type_of_global_in_context env r = - match r with - | VarRef id -> Environ.named_type id env, Univ.AUContext.empty - | ConstRef c -> - let cb = Environ.lookup_constant c env in - let univs = Declareops.constant_polymorphic_context cb in - cb.Declarations.const_type, univs - | IndRef ind -> - let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - let univs = Declareops.inductive_polymorphic_context mib in - let inst = Univ.make_abstract_instance univs in - let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in - Inductive.type_of_inductive env (specif, inst), univs - | ConstructRef cstr -> - let (mib,oib as specif) = - Inductive.lookup_mind_specif env (inductive_of_constructor cstr) - in - let univs = Declareops.inductive_polymorphic_context mib in - let inst = Univ.make_abstract_instance univs in - Inductive.type_of_constructor (cstr,inst) specif, univs +let constr_of_global_in_context = Typeops.constr_of_global_in_context +let type_of_global_in_context = Typeops.type_of_global_in_context let universes_of_global gr = universes_of_global (env ()) gr diff --git a/library/global.mli b/library/global.mli index 29255a70ff..42a8005a4f 100644 --- a/library/global.mli +++ b/library/global.mli @@ -129,17 +129,11 @@ val is_type_in_type : GlobRef.t -> bool val constr_of_global_in_context : Environ.env -> GlobRef.t -> Constr.types * Univ.AUContext.t -(** Returns the type of the constant in its local universe - context. The type should not be used without pushing it's universe - context in the environmnent of usage. For non-universe-polymorphic - constants, it does not matter. *) + [@@ocaml.deprecated "alias of [Typeops.constr_of_global_in_context]"] val type_of_global_in_context : Environ.env -> GlobRef.t -> Constr.types * Univ.AUContext.t -(** Returns the type of the constant in its local universe - context. The type should not be used without pushing it's universe - context in the environmnent of usage. For non-universe-polymorphic - constants, it does not matter. *) + [@@ocaml.deprecated "alias of [Typeops.type_of_global]"] (** Returns the universe context of the global reference (whatever its polymorphic status is). *) val universes_of_global : GlobRef.t -> Univ.AUContext.t |