From b0ef649660542ae840ea945d7ab4f1f3ae7b85cd Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 28 Apr 2018 17:58:08 +0200 Subject: Split off Universes functions dealing with names. This API is a bit strange, I expect it will change at some point. --- interp/declare.ml | 6 +++--- interp/declare.mli | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) (limited to 'interp') diff --git a/interp/declare.ml b/interp/declare.ml index c55a6c69b..34bf5c8a2 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -487,7 +487,7 @@ let add_universe src (dp, i) = Option.iter (fun poly -> let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in Global.push_context_set poly ctx; - Universes.add_global_universe level poly; + UnivNames.add_global_universe level poly; if poly then Lib.add_section_context ctx) optpoly @@ -538,7 +538,7 @@ let input_universe : universe_decl -> Libobject.obj = let declare_univ_binders gr pl = if Global.is_polymorphic gr then - Universes.register_universe_binders gr pl + UnivNames.register_universe_binders gr pl else let l = match gr with | ConstRef c -> Label.to_id @@ Constant.label c @@ -595,7 +595,7 @@ let input_constraints : constraint_decl -> Libobject.obj = let do_constraint poly l = let u_of_id x = let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in - Universes.is_polymorphic level, level + UnivNames.is_polymorphic level, level in let in_section = Lib.sections_are_opened () in let () = diff --git a/interp/declare.mli b/interp/declare.mli index f8cffbb1e..0d795c497 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -83,7 +83,7 @@ val recursive_message : bool (** true = fixpoint *) -> val exists_name : Id.t -> bool (** Global universe contexts, names and constraints *) -val declare_univ_binders : GlobRef.t -> Universes.universe_binders -> unit +val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit -- cgit v1.2.3 From a51dda2344679dc6d9145f3f34acad29721f6c75 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 28 Apr 2018 19:26:21 +0200 Subject: Split off Universes functions dealing with generating new universes. --- engine/engine.mllib | 1 + engine/evd.ml | 10 +- engine/uState.ml | 4 +- engine/univGen.ml | 246 +++++++++++++++++++++++ engine/univGen.mli | 80 ++++++++ engine/universes.ml | 264 +++---------------------- engine/universes.mli | 154 ++++++++------- interp/declare.ml | 2 +- plugins/btauto/refl_btauto.ml | 4 +- plugins/extraction/extraction.ml | 2 +- plugins/firstorder/rules.ml | 2 +- plugins/fourier/fourierR.ml | 8 +- plugins/funind/functional_principles_proofs.ml | 8 +- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/indfun_common.ml | 8 +- plugins/funind/invfun.ml | 4 +- plugins/funind/recdef.ml | 6 +- plugins/micromega/coq_micromega.ml | 2 +- plugins/nsatz/nsatz.ml | 2 +- plugins/omega/coq_omega.ml | 2 +- plugins/quote/quote.ml | 2 +- plugins/romega/const_omega.ml | 10 +- plugins/rtauto/refl_tauto.ml | 8 +- plugins/setoid_ring/newring.ml | 8 +- plugins/ssr/ssrcommon.ml | 2 +- plugins/ssr/ssrequality.ml | 4 +- pretyping/classops.ml | 4 +- pretyping/evarconv.ml | 4 +- pretyping/indrec.ml | 4 +- pretyping/reductionops.ml | 4 +- pretyping/typeclasses.ml | 4 +- proofs/tacmach.ml | 2 +- stm/asyncTaskQueue.ml | 6 +- tactics/auto.ml | 2 +- tactics/autorewrite.ml | 2 +- tactics/class_tactics.ml | 2 +- tactics/eauto.ml | 2 +- tactics/eqschemes.ml | 24 +-- tactics/equality.ml | 4 +- tactics/hints.ml | 2 +- vernac/auto_ind_decl.ml | 12 +- vernac/comAssumption.ml | 2 +- vernac/indschemes.ml | 2 +- vernac/obligations.ml | 2 +- 44 files changed, 533 insertions(+), 396 deletions(-) create mode 100644 engine/univGen.ml create mode 100644 engine/univGen.mli (limited to 'interp') diff --git a/engine/engine.mllib b/engine/engine.mllib index 207dbde1e..512908e13 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -1,4 +1,5 @@ UnivNames +UnivGen Universes Univops UState diff --git a/engine/evd.ml b/engine/evd.ml index 20a7c80ea..b2b8e7ccc 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -804,19 +804,19 @@ let make_flexible_variable evd ~algebraic u = (****************************************) let fresh_sort_in_family ?loc ?(rigid=univ_flexible) env evd s = - with_context_set ?loc rigid evd (Universes.fresh_sort_in_family env s) + with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family env s) let fresh_constant_instance ?loc env evd c = - with_context_set ?loc univ_flexible evd (Universes.fresh_constant_instance env c) + with_context_set ?loc univ_flexible evd (UnivGen.fresh_constant_instance env c) let fresh_inductive_instance ?loc env evd i = - with_context_set ?loc univ_flexible evd (Universes.fresh_inductive_instance env i) + with_context_set ?loc univ_flexible evd (UnivGen.fresh_inductive_instance env i) let fresh_constructor_instance ?loc env evd c = - with_context_set ?loc univ_flexible evd (Universes.fresh_constructor_instance env c) + with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c) let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr = - with_context_set ?loc rigid evd (Universes.fresh_global_instance ?names env gr) + with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?names env gr) let whd_sort_variable evd t = t diff --git a/engine/uState.ml b/engine/uState.ml index ffb54d441..839bb5ae9 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -471,7 +471,7 @@ let emit_side_effects eff u = let new_univ_variable ?loc rigid name ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = - let u = Universes.new_univ_level () in + let u = UnivGen.new_univ_level () in let ctx' = Univ.ContextSet.add_universe u ctx in let uctx', pred = match rigid with @@ -582,7 +582,7 @@ let fix_undefined_variables uctx = uctx_univ_algebraic = algs' } let refresh_undefined_univ_variables uctx = - let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in + let subst, ctx' = UnivGen.fresh_universe_context_set_instance uctx.uctx_local in let subst_fn u = Univ.subst_univs_level_level subst u in let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (subst_fn u) acc) uctx.uctx_univ_algebraic Univ.LSet.empty diff --git a/engine/univGen.ml b/engine/univGen.ml new file mode 100644 index 000000000..796a1bcc1 --- /dev/null +++ b/engine/univGen.ml @@ -0,0 +1,246 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Global.current_dirpath (), n) + +let new_univ_level () = + let dp, id = new_univ_id () in + Univ.Level.make dp id + +let fresh_level () = new_univ_level () + +(* TODO: remove *) +let new_univ dp = Univ.Universe.make (new_univ_level dp) +let new_Type dp = mkType (new_univ dp) +let new_Type_sort dp = Type (new_univ dp) + +let fresh_universe_instance ctx = + let init _ = new_univ_level () in + Instance.of_array (Array.init (AUContext.size ctx) init) + +let fresh_instance_from_context ctx = + let inst = fresh_universe_instance ctx in + let constraints = AUContext.instantiate inst ctx in + inst, constraints + +let fresh_instance ctx = + let ctx' = ref LSet.empty in + let init _ = + let u = new_univ_level () in + ctx' := LSet.add u !ctx'; u + in + let inst = Instance.of_array (Array.init (AUContext.size ctx) init) + in !ctx', inst + +let existing_instance ctx inst = + let () = + let len1 = Array.length (Instance.to_array inst) + and len2 = AUContext.size ctx in + if not (len1 == len2) then + CErrors.user_err ~hdr:"Universes" + Pp.(str "Polymorphic constant expected " ++ int len2 ++ + str" levels but was given " ++ int len1) + else () + in LSet.empty, inst + +let fresh_instance_from ctx inst = + let ctx', inst = + match inst with + | Some inst -> existing_instance ctx inst + | None -> fresh_instance ctx + in + let constraints = AUContext.instantiate inst ctx in + inst, (ctx', constraints) + +(** Fresh universe polymorphic construction *) + +let fresh_constant_instance env c inst = + let cb = lookup_constant c env in + match cb.Declarations.const_universes with + | Declarations.Monomorphic_const _ -> ((c,Instance.empty), ContextSet.empty) + | Declarations.Polymorphic_const auctx -> + let inst, ctx = + fresh_instance_from auctx inst + in + ((c, inst), ctx) + +let fresh_inductive_instance env ind inst = + let mib, mip = Inductive.lookup_mind_specif env ind in + match mib.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> + ((ind,Instance.empty), ContextSet.empty) + | Declarations.Polymorphic_ind uactx -> + let inst, ctx = (fresh_instance_from uactx) inst in + ((ind,inst), ctx) + | Declarations.Cumulative_ind acumi -> + let inst, ctx = + fresh_instance_from (Univ.ACumulativityInfo.univ_context acumi) inst + in ((ind,inst), ctx) + +let fresh_constructor_instance env (ind,i) inst = + let mib, mip = Inductive.lookup_mind_specif env ind in + match mib.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> (((ind,i),Instance.empty), ContextSet.empty) + | Declarations.Polymorphic_ind auctx -> + let inst, ctx = fresh_instance_from auctx inst in + (((ind,i),inst), ctx) + | Declarations.Cumulative_ind acumi -> + let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in + (((ind,i),inst), ctx) + +open Globnames + +let fresh_global_instance ?names env gr = + match gr with + | VarRef id -> mkVar id, ContextSet.empty + | ConstRef sp -> + let c, ctx = fresh_constant_instance env sp names in + mkConstU c, ctx + | ConstructRef sp -> + let c, ctx = fresh_constructor_instance env sp names in + mkConstructU c, ctx + | IndRef sp -> + let c, ctx = fresh_inductive_instance env sp names in + mkIndU c, ctx + +let fresh_constant_instance env sp = + fresh_constant_instance env sp None + +let fresh_inductive_instance env sp = + fresh_inductive_instance env sp None + +let fresh_constructor_instance env sp = + fresh_constructor_instance env sp None + +let constr_of_global gr = + let c, ctx = fresh_global_instance (Global.env ()) gr in + if not (Univ.ContextSet.is_empty ctx) then + if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then + (* Should be an error as we might forget constraints, allow for now + to make firstorder work with "using" clauses *) + c + else CErrors.user_err ~hdr:"constr_of_global" + Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ + str " would forget universes.") + else c + +let constr_of_global_univ (gr,u) = + match gr with + | VarRef id -> mkVar id + | ConstRef sp -> mkConstU (sp,u) + | ConstructRef sp -> mkConstructU (sp,u) + | IndRef sp -> mkIndU (sp,u) + +let fresh_global_or_constr_instance env = function + | IsConstr c -> c, ContextSet.empty + | IsGlobal gr -> fresh_global_instance env gr + +let global_of_constr c = + match kind c with + | Const (c, u) -> ConstRef c, u + | Ind (i, u) -> IndRef i, u + | Construct (c, u) -> ConstructRef c, u + | Var id -> VarRef id, Instance.empty + | _ -> raise Not_found + +open Declarations + +let type_of_reference env r = + match r with + | VarRef id -> Environ.named_type id env, ContextSet.empty + | ConstRef c -> + let cb = Environ.lookup_constant c env in + let ty = cb.const_type in + begin + match cb.const_universes with + | Monomorphic_const _ -> ty, ContextSet.empty + | Polymorphic_const auctx -> + let inst, ctx = fresh_instance_from auctx None in + Vars.subst_instance_constr inst ty, ctx + end + | IndRef ind -> + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in + begin + match mib.mind_universes with + | Monomorphic_ind _ -> + let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in + ty, ContextSet.empty + | Polymorphic_ind auctx -> + let inst, ctx = fresh_instance_from auctx None in + let ty = Inductive.type_of_inductive env (specif, inst) in + ty, ctx + | Cumulative_ind cumi -> + let inst, ctx = + fresh_instance_from (ACumulativityInfo.univ_context cumi) None + in + let ty = Inductive.type_of_inductive env (specif, inst) in + ty, ctx + end + + | ConstructRef cstr -> + let (mib,oib as specif) = + Inductive.lookup_mind_specif env (inductive_of_constructor cstr) + in + begin + match mib.mind_universes with + | Monomorphic_ind _ -> + Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty + | Polymorphic_ind auctx -> + let inst, ctx = fresh_instance_from auctx None in + Inductive.type_of_constructor (cstr,inst) specif, ctx + | Cumulative_ind cumi -> + let inst, ctx = + fresh_instance_from (ACumulativityInfo.univ_context cumi) None + in + Inductive.type_of_constructor (cstr,inst) specif, ctx + end + +let type_of_global t = type_of_reference (Global.env ()) t + +let fresh_sort_in_family env = function + | InProp -> Sorts.prop, ContextSet.empty + | InSet -> Sorts.set, ContextSet.empty + | InType -> + let u = fresh_level () in + Type (Univ.Universe.make u), ContextSet.singleton u + +let new_sort_in_family sf = + fst (fresh_sort_in_family (Global.env ()) sf) + +let extend_context (a, ctx) (ctx') = + (a, ContextSet.union ctx ctx') + +let new_global_univ () = + let u = fresh_level () in + (Univ.Universe.make u, ContextSet.singleton u) + +let fresh_universe_context_set_instance ctx = + if ContextSet.is_empty ctx then LMap.empty, ctx + else + let (univs, cst) = ContextSet.levels ctx, ContextSet.constraints ctx in + let univs',subst = LSet.fold + (fun u (univs',subst) -> + let u' = fresh_level () in + (LSet.add u' univs', LMap.add u u' subst)) + univs (LSet.empty, LMap.empty) + in + let cst' = subst_univs_level_constraints subst cst in + subst, (univs', cst') diff --git a/engine/univGen.mli b/engine/univGen.mli new file mode 100644 index 000000000..8169dbda4 --- /dev/null +++ b/engine/univGen.mli @@ -0,0 +1,80 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* universe_id +val new_univ_level : unit -> Level.t +val new_univ : unit -> Universe.t +val new_Type : unit -> types +val new_Type_sort : unit -> Sorts.t + +val new_global_univ : unit -> Universe.t in_universe_context_set +val new_sort_in_family : Sorts.family -> Sorts.t + +(** Build a fresh instance for a given context, its associated substitution and + the instantiated constraints. *) + +val fresh_instance_from_context : AUContext.t -> + Instance.t constrained + +val fresh_instance_from : AUContext.t -> Instance.t option -> + Instance.t in_universe_context_set + +val fresh_sort_in_family : env -> Sorts.family -> + Sorts.t in_universe_context_set +val fresh_constant_instance : env -> Constant.t -> + pconstant in_universe_context_set +val fresh_inductive_instance : env -> inductive -> + pinductive in_universe_context_set +val fresh_constructor_instance : env -> constructor -> + pconstructor in_universe_context_set + +val fresh_global_instance : ?names:Univ.Instance.t -> env -> GlobRef.t -> + constr in_universe_context_set + +val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> + constr in_universe_context_set + +(** Get fresh variables for the universe context. + Useful to make tactics that manipulate constrs in universe contexts polymorphic. *) +val fresh_universe_context_set_instance : ContextSet.t -> + universe_level_subst * ContextSet.t + +(** Raises [Not_found] if not a global reference. *) +val global_of_constr : constr -> GlobRef.t puniverses + +val constr_of_global_univ : GlobRef.t puniverses -> constr + +val extend_context : 'a in_universe_context_set -> ContextSet.t -> + 'a in_universe_context_set + +(** Create a fresh global in the global environment, without side effects. + BEWARE: this raises an ANOMALY on polymorphic constants/inductives: + the constraints should be properly added to an evd. + See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for + the proper way to get a fresh copy of a global reference. *) +val constr_of_global : GlobRef.t -> constr + +(** Returns the type of the global reference, by creating a fresh instance of polymorphic + references and computing their instantiated universe context. (side-effect on the + universe counter, use with care). *) +val type_of_global : GlobRef.t -> types in_universe_context_set diff --git a/engine/universes.ml b/engine/universes.ml index 1dccde025..29c9bd017 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -11,9 +11,7 @@ open Sorts open Util open Pp -open Names open Constr -open Environ open Univ (* To disallow minimization to Set *) @@ -214,226 +212,6 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu = let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' 0 m n in if res then Some !cstrs else None -(* Generator of levels *) -type universe_id = DirPath.t * int - -let new_univ_id, set_remote_new_univ_id = - RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1) - ~build:(fun n -> Global.current_dirpath (), n) - -let new_univ_level () = - let dp, id = new_univ_id () in - Univ.Level.make dp id - -let fresh_level () = new_univ_level () - -(* TODO: remove *) -let new_univ dp = Univ.Universe.make (new_univ_level dp) -let new_Type dp = mkType (new_univ dp) -let new_Type_sort dp = Type (new_univ dp) - -let fresh_universe_instance ctx = - let init _ = new_univ_level () in - Instance.of_array (Array.init (AUContext.size ctx) init) - -let fresh_instance_from_context ctx = - let inst = fresh_universe_instance ctx in - let constraints = AUContext.instantiate inst ctx in - inst, constraints - -let fresh_instance ctx = - let ctx' = ref LSet.empty in - let init _ = - let u = new_univ_level () in - ctx' := LSet.add u !ctx'; u - in - let inst = Instance.of_array (Array.init (AUContext.size ctx) init) - in !ctx', inst - -let existing_instance ctx inst = - let () = - let len1 = Array.length (Instance.to_array inst) - and len2 = AUContext.size ctx in - if not (len1 == len2) then - CErrors.user_err ~hdr:"Universes" - (str "Polymorphic constant expected " ++ int len2 ++ - str" levels but was given " ++ int len1) - else () - in LSet.empty, inst - -let fresh_instance_from ctx inst = - let ctx', inst = - match inst with - | Some inst -> existing_instance ctx inst - | None -> fresh_instance ctx - in - let constraints = AUContext.instantiate inst ctx in - inst, (ctx', constraints) - -(** Fresh universe polymorphic construction *) - -let fresh_constant_instance env c inst = - let cb = lookup_constant c env in - match cb.Declarations.const_universes with - | Declarations.Monomorphic_const _ -> ((c,Instance.empty), ContextSet.empty) - | Declarations.Polymorphic_const auctx -> - let inst, ctx = - fresh_instance_from auctx inst - in - ((c, inst), ctx) - -let fresh_inductive_instance env ind inst = - let mib, mip = Inductive.lookup_mind_specif env ind in - match mib.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - ((ind,Instance.empty), ContextSet.empty) - | Declarations.Polymorphic_ind uactx -> - let inst, ctx = (fresh_instance_from uactx) inst in - ((ind,inst), ctx) - | Declarations.Cumulative_ind acumi -> - let inst, ctx = - fresh_instance_from (Univ.ACumulativityInfo.univ_context acumi) inst - in ((ind,inst), ctx) - -let fresh_constructor_instance env (ind,i) inst = - let mib, mip = Inductive.lookup_mind_specif env ind in - match mib.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> (((ind,i),Instance.empty), ContextSet.empty) - | Declarations.Polymorphic_ind auctx -> - let inst, ctx = fresh_instance_from auctx inst in - (((ind,i),inst), ctx) - | Declarations.Cumulative_ind acumi -> - let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in - (((ind,i),inst), ctx) - -open Globnames - -let fresh_global_instance ?names env gr = - match gr with - | VarRef id -> mkVar id, ContextSet.empty - | ConstRef sp -> - let c, ctx = fresh_constant_instance env sp names in - mkConstU c, ctx - | ConstructRef sp -> - let c, ctx = fresh_constructor_instance env sp names in - mkConstructU c, ctx - | IndRef sp -> - let c, ctx = fresh_inductive_instance env sp names in - mkIndU c, ctx - -let fresh_constant_instance env sp = - fresh_constant_instance env sp None - -let fresh_inductive_instance env sp = - fresh_inductive_instance env sp None - -let fresh_constructor_instance env sp = - fresh_constructor_instance env sp None - -let constr_of_global gr = - let c, ctx = fresh_global_instance (Global.env ()) gr in - if not (Univ.ContextSet.is_empty ctx) then - if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then - (* Should be an error as we might forget constraints, allow for now - to make firstorder work with "using" clauses *) - c - else CErrors.user_err ~hdr:"constr_of_global" - Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ - str " would forget universes.") - else c - -let constr_of_reference = constr_of_global - -let constr_of_global_univ (gr,u) = - match gr with - | VarRef id -> mkVar id - | ConstRef sp -> mkConstU (sp,u) - | ConstructRef sp -> mkConstructU (sp,u) - | IndRef sp -> mkIndU (sp,u) - -let fresh_global_or_constr_instance env = function - | IsConstr c -> c, ContextSet.empty - | IsGlobal gr -> fresh_global_instance env gr - -let global_of_constr c = - match kind c with - | Const (c, u) -> ConstRef c, u - | Ind (i, u) -> IndRef i, u - | Construct (c, u) -> ConstructRef c, u - | Var id -> VarRef id, Instance.empty - | _ -> raise Not_found - -open Declarations - -let type_of_reference env r = - match r with - | VarRef id -> Environ.named_type id env, ContextSet.empty - | ConstRef c -> - let cb = Environ.lookup_constant c env in - let ty = cb.const_type in - begin - match cb.const_universes with - | Monomorphic_const _ -> ty, ContextSet.empty - | Polymorphic_const auctx -> - let inst, ctx = fresh_instance_from auctx None in - Vars.subst_instance_constr inst ty, ctx - end - | IndRef ind -> - let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - begin - match mib.mind_universes with - | Monomorphic_ind _ -> - let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in - ty, ContextSet.empty - | Polymorphic_ind auctx -> - let inst, ctx = fresh_instance_from auctx None in - let ty = Inductive.type_of_inductive env (specif, inst) in - ty, ctx - | Cumulative_ind cumi -> - let inst, ctx = - fresh_instance_from (ACumulativityInfo.univ_context cumi) None - in - let ty = Inductive.type_of_inductive env (specif, inst) in - ty, ctx - end - - | ConstructRef cstr -> - let (mib,oib as specif) = - Inductive.lookup_mind_specif env (inductive_of_constructor cstr) - in - begin - match mib.mind_universes with - | Monomorphic_ind _ -> - Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty - | Polymorphic_ind auctx -> - let inst, ctx = fresh_instance_from auctx None in - Inductive.type_of_constructor (cstr,inst) specif, ctx - | Cumulative_ind cumi -> - let inst, ctx = - fresh_instance_from (ACumulativityInfo.univ_context cumi) None - in - Inductive.type_of_constructor (cstr,inst) specif, ctx - end - -let type_of_global t = type_of_reference (Global.env ()) t - -let fresh_sort_in_family env = function - | InProp -> Sorts.prop, ContextSet.empty - | InSet -> Sorts.set, ContextSet.empty - | InType -> - let u = fresh_level () in - Type (Univ.Universe.make u), ContextSet.singleton u - -let new_sort_in_family sf = - fst (fresh_sort_in_family (Global.env ()) sf) - -let extend_context (a, ctx) (ctx') = - (a, ContextSet.union ctx ctx') - -let new_global_univ () = - let u = fresh_level () in - (Univ.Universe.make u, ContextSet.singleton u) - (** Simplification *) let add_list_map u t map = @@ -504,19 +282,6 @@ let subst_univs_constr = CProfile.profile2 subst_univs_constr_key subst_univs_constr else subst_univs_constr -let fresh_universe_context_set_instance ctx = - if ContextSet.is_empty ctx then LMap.empty, ctx - else - let (univs, cst) = ContextSet.levels ctx, ContextSet.constraints ctx in - let univs',subst = LSet.fold - (fun u (univs',subst) -> - let u' = fresh_level () in - (LSet.add u' univs', LMap.add u u' subst)) - univs (LSet.empty, LMap.empty) - in - let cst' = subst_univs_level_constraints subst cst in - subst, (univs', cst') - let normalize_univ_variable ~find = let rec aux cur = let b = find cur in @@ -1020,6 +785,8 @@ let solve_constraints_system levels level_bounds level_min = v (** Deprecated *) + +(** UnivNames *) type universe_binders = UnivNames.universe_binders type univ_name_list = UnivNames.univ_name_list @@ -1036,3 +803,30 @@ let register_universe_binders = UnivNames.register_universe_binders let universe_binders_of_global = UnivNames.universe_binders_of_global let universe_binders_with_opt_names = UnivNames.universe_binders_with_opt_names + +(** UnivGen *) +type universe_id = UnivGen.universe_id + +let set_remote_new_univ_id = UnivGen.set_remote_new_univ_id +let new_univ_id = UnivGen.new_univ_id +let new_univ_level = UnivGen.new_univ_level +let new_univ = UnivGen.new_univ +let new_Type = UnivGen.new_Type +let new_Type_sort = UnivGen.new_Type_sort +let new_global_univ = UnivGen.new_global_univ +let new_sort_in_family = UnivGen.new_sort_in_family +let fresh_instance_from_context = UnivGen.fresh_instance_from_context +let fresh_instance_from = UnivGen.fresh_instance_from +let fresh_sort_in_family = UnivGen.fresh_sort_in_family +let fresh_constant_instance = UnivGen.fresh_constant_instance +let fresh_inductive_instance = UnivGen.fresh_inductive_instance +let fresh_constructor_instance = UnivGen.fresh_constructor_instance +let fresh_global_instance = UnivGen.fresh_global_instance +let fresh_global_or_constr_instance = UnivGen.fresh_global_or_constr_instance +let fresh_universe_context_set_instance = UnivGen.fresh_universe_context_set_instance +let global_of_constr = UnivGen.global_of_constr +let constr_of_global_univ = UnivGen.constr_of_global_univ +let extend_context = UnivGen.extend_context +let constr_of_global = UnivGen.constr_of_global +let constr_of_reference = UnivGen.constr_of_global +let type_of_global = UnivGen.type_of_global diff --git a/engine/universes.mli b/engine/universes.mli index aaf295c1d..da4a00751 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -19,22 +19,6 @@ module UPairSet : CSet.S with type elt = (Level.t * Level.t) (** Universes *) -(** The global universe counter *) -type universe_id = DirPath.t * int - -val set_remote_new_univ_id : universe_id RemoteCounter.installer - -(** Side-effecting functions creating new universe levels. *) - -val new_univ_id : unit -> universe_id -val new_univ_level : unit -> Level.t -val new_univ : unit -> Universe.t -val new_Type : unit -> types -val new_Type_sort : unit -> Sorts.t - -val new_global_univ : unit -> Universe.t in_universe_context_set -val new_sort_in_family : Sorts.family -> Sorts.t - (** {6 Constraints for type inference} When doing conversion of universes, not only do we have =/<= constraints but @@ -82,43 +66,6 @@ val eq_constr_univs_infer_with : (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option -(** Build a fresh instance for a given context, its associated substitution and - the instantiated constraints. *) - -val fresh_instance_from_context : AUContext.t -> - Instance.t constrained - -val fresh_instance_from : AUContext.t -> Instance.t option -> - Instance.t in_universe_context_set - -val fresh_sort_in_family : env -> Sorts.family -> - Sorts.t in_universe_context_set -val fresh_constant_instance : env -> Constant.t -> - pconstant in_universe_context_set -val fresh_inductive_instance : env -> inductive -> - pinductive in_universe_context_set -val fresh_constructor_instance : env -> constructor -> - pconstructor in_universe_context_set - -val fresh_global_instance : ?names:Univ.Instance.t -> env -> GlobRef.t -> - constr in_universe_context_set - -val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> - constr in_universe_context_set - -(** Get fresh variables for the universe context. - Useful to make tactics that manipulate constrs in universe contexts polymorphic. *) -val fresh_universe_context_set_instance : ContextSet.t -> - universe_level_subst * ContextSet.t - -(** Raises [Not_found] if not a global reference. *) -val global_of_constr : constr -> GlobRef.t puniverses - -val constr_of_global_univ : GlobRef.t puniverses -> constr - -val extend_context : 'a in_universe_context_set -> ContextSet.t -> - 'a in_universe_context_set - (** Simplification and pruning of constraints: [normalize_context_set ctx us] @@ -166,22 +113,6 @@ val normalize_universe_opt_subst : universe_opt_subst -> val normalize_universe_subst : universe_subst -> (Universe.t -> Universe.t) -(** Create a fresh global in the global environment, without side effects. - BEWARE: this raises an ANOMALY on polymorphic constants/inductives: - the constraints should be properly added to an evd. - See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for - the proper way to get a fresh copy of a global reference. *) -val constr_of_global : GlobRef.t -> constr - -(** ** DEPRECATED ** synonym of [constr_of_global] *) -val constr_of_reference : GlobRef.t -> constr -[@@ocaml.deprecated "synonym of [constr_of_global]"] - -(** Returns the type of the global reference, by creating a fresh instance of polymorphic - references and computing their instantiated universe context. (side-effect on the - universe counter, use with care). *) -val type_of_global : GlobRef.t -> types in_universe_context_set - (** Full universes substitutions into terms *) val nf_evars_and_universes_opt_subst : (existential -> constr option) -> @@ -199,6 +130,7 @@ val solve_constraints_system : Universe.t option array -> Universe.t array -> Un Universe.t array (** *********************************** Deprecated *) + [@@@ocaml.warning "-3"] val set_minimization : bool ref [@@ocaml.deprecated "Becoming internal."] @@ -235,3 +167,87 @@ type univ_name_list = UnivNames.univ_name_list val universe_binders_with_opt_names : Globnames.global_reference -> Univ.Level.t list -> univ_name_list option -> universe_binders [@@ocaml.deprecated "Use [UnivNames.universe_binders_with_opt_names]"] + +(** ****** Deprecated: moved to [UnivGen] *) + +type universe_id = UnivGen.universe_id +[@@ocaml.deprecated "Use [UnivGen.universe_id]"] + +val set_remote_new_univ_id : universe_id RemoteCounter.installer +[@@ocaml.deprecated "Use [UnivGen.set_remote_new_univ_id]"] + +val new_univ_id : unit -> universe_id +[@@ocaml.deprecated "Use [UnivGen.new_univ_id]"] + +val new_univ_level : unit -> Level.t +[@@ocaml.deprecated "Use [UnivGen.new_univ_level]"] + +val new_univ : unit -> Universe.t +[@@ocaml.deprecated "Use [UnivGen.new_univ]"] + +val new_Type : unit -> types +[@@ocaml.deprecated "Use [UnivGen.new_Type]"] + +val new_Type_sort : unit -> Sorts.t +[@@ocaml.deprecated "Use [UnivGen.new_Type_sort]"] + +val new_global_univ : unit -> Universe.t in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.new_global_univ]"] + +val new_sort_in_family : Sorts.family -> Sorts.t +[@@ocaml.deprecated "Use [UnivGen.new_sort_in_family]"] + +val fresh_instance_from_context : AUContext.t -> + Instance.t constrained +[@@ocaml.deprecated "Use [UnivGen.fresh_instance_from_context]"] + +val fresh_instance_from : AUContext.t -> Instance.t option -> + Instance.t in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.fresh_instance_from]"] + +val fresh_sort_in_family : env -> Sorts.family -> + Sorts.t in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.fresh_sort_in_family]"] + +val fresh_constant_instance : env -> Constant.t -> + pconstant in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.fresh_constant_instance]"] + +val fresh_inductive_instance : env -> inductive -> + pinductive in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.fresh_inductive_instance]"] + +val fresh_constructor_instance : env -> constructor -> + pconstructor in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.fresh_constructor_instance]"] + +val fresh_global_instance : ?names:Univ.Instance.t -> env -> Globnames.global_reference -> + constr in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.fresh_global_instance]"] + +val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> + constr in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.fresh_global_or_constr_instance]"] + +val fresh_universe_context_set_instance : ContextSet.t -> + universe_level_subst * ContextSet.t +[@@ocaml.deprecated "Use [UnivGen.fresh_universe_context_set_instance]"] + +val global_of_constr : constr -> Globnames.global_reference puniverses +[@@ocaml.deprecated "Use [UnivGen.global_of_constr]"] + +val constr_of_global_univ : Globnames.global_reference puniverses -> constr +[@@ocaml.deprecated "Use [UnivGen.constr_of_global_univ]"] + +val extend_context : 'a in_universe_context_set -> ContextSet.t -> + 'a in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.extend_context]"] + +val constr_of_global : Globnames.global_reference -> constr +[@@ocaml.deprecated "Use [UnivGen.constr_of_global]"] + +val constr_of_reference : Globnames.global_reference -> constr +[@@ocaml.deprecated "Use [UnivGen.constr_of_global]"] + +val type_of_global : Globnames.global_reference -> types in_universe_context_set +[@@ocaml.deprecated "Use [UnivGen.type_of_global]"] diff --git a/interp/declare.ml b/interp/declare.ml index 34bf5c8a2..bc2d2068a 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -564,7 +564,7 @@ let do_universe poly l = in let l = List.map (fun {CAst.v=id} -> - let lev = Universes.new_univ_id () in + let lev = UnivGen.new_univ_id () in (id, lev)) l in let src = if poly then BoundUniv else UnqualifiedUniv in diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index a09abfa19..7f98ed427 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -2,11 +2,11 @@ let contrib_name = "btauto" let init_constant dir s = let find_constant contrib dir s = - Universes.constr_of_global (Coqlib.find_reference contrib dir s) + UnivGen.constr_of_global (Coqlib.find_reference contrib dir s) in find_constant contrib_name dir s -let get_constant dir s = lazy (Universes.constr_of_global @@ Coqlib.coq_reference contrib_name dir s) +let get_constant dir s = lazy (UnivGen.constr_of_global @@ Coqlib.coq_reference contrib_name dir s) let get_inductive dir s = let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index f25f63624..cdd698304 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -431,7 +431,7 @@ and extract_really_ind env kn mib = let packets = Array.mapi (fun i mip -> - let (_,u),_ = Universes.fresh_inductive_instance env (kn,i) in + let (_,u),_ = UnivGen.fresh_inductive_instance env (kn,i) in let ar = Inductive.type_of_inductive env ((mib,mip),u) in let ar = EConstr.of_constr ar in let info = (fst (flag_of_type env sg ar) = Info) in diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 2d7a3e37b..b13580bc0 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -233,7 +233,7 @@ let ll_forall_tac prod backtrack id continue seq= (* special for compatibility with old Intuition *) -let constant str = Universes.constr_of_global +let constant str = UnivGen.constr_of_global @@ Coqlib.coq_reference "User" ["Init";"Logic"] str let defined_connectives=lazy diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 0ea70c19f..96be1d893 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -283,15 +283,15 @@ let fourier_lineq lineq1 = let get = Lazy.force let cget = get let eget c = EConstr.of_constr (Lazy.force c) -let constant path s = Universes.constr_of_global @@ +let constant path s = UnivGen.constr_of_global @@ Coqlib.coq_reference "Fourier" path s (* Standard library *) open Coqlib let coq_sym_eqT = lazy (build_coq_eq_sym ()) -let coq_False = lazy (Universes.constr_of_global @@ build_coq_False ()) -let coq_not = lazy (Universes.constr_of_global @@ build_coq_not ()) -let coq_eq = lazy (Universes.constr_of_global @@ build_coq_eq ()) +let coq_False = lazy (UnivGen.constr_of_global @@ build_coq_False ()) +let coq_not = lazy (UnivGen.constr_of_global @@ build_coq_not ()) +let coq_eq = lazy (UnivGen.constr_of_global @@ build_coq_eq ()) (* Rdefinitions *) let constant_real = constant ["Reals";"Rdefinitions"] diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 44fa0740d..3801fec4b 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -414,9 +414,9 @@ let rewrite_until_var arg_num eq_ids : tactic = let rec_pte_id = Id.of_string "Hrec" let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = - let coq_False = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ()) in - let coq_True = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_True ()) in - let coq_I = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_I ()) in + let coq_False = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_False ()) in + let coq_True = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_True ()) in + let coq_I = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_I ()) in let rec scan_type context type_of_hyp : tactic = if isLetIn sigma type_of_hyp then let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in @@ -1603,7 +1603,7 @@ let prove_principle_for_gen match !tcc_lemma_ref with | Undefined -> user_err Pp.(str "No tcc proof !!") | Value lemma -> EConstr.of_constr lemma - | Not_needed -> EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_I ()) + | Not_needed -> EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_I ()) in (* let rec list_diff del_list check_list = *) (* match del_list with *) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index dc0f240bd..a158fc8ff 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -689,7 +689,7 @@ let build_case_scheme fa = let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in let sorts = (fun (_,_,x) -> - Universes.new_sort_in_family x + UnivGen.new_sort_in_family x ) fa in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index a0b9217c7..35c3acd41 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -117,7 +117,7 @@ let def_of_const t = |_ -> assert false let coq_constant s = - Universes.constr_of_global @@ + UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s;; @@ -471,7 +471,7 @@ let jmeq () = try Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ - Universes.constr_of_global @@ + UnivGen.constr_of_global @@ Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq" with e when CErrors.noncritical e -> raise (ToShow e) @@ -479,7 +479,7 @@ let jmeq_refl () = try Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ - Universes.constr_of_global @@ + UnivGen.constr_of_global @@ Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq_refl" with e when CErrors.noncritical e -> raise (ToShow e) @@ -492,7 +492,7 @@ let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded" let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc") let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv") -let well_founded_ltof () = EConstr.of_constr @@ Universes.constr_of_global @@ +let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_global @@ Coqlib.coq_reference "" ["Arith";"Wf_nat"] "well_founded_ltof" let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof") diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 094f54156..180952635 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -81,7 +81,7 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl let make_eq () = try - EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ())) + EConstr.of_constr (UnivGen.constr_of_global (Coqlib.build_coq_eq ())) with _ -> assert false @@ -512,7 +512,7 @@ and intros_with_rewrite_aux : Tacmach.tactic = intros_with_rewrite ] g end - | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ())) -> + | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_False ())) -> Proofview.V82.of_tactic tauto g | Case(_,_,v,_) -> tclTHENLIST[ diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 2a3a85fcc..2464c595f 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -49,7 +49,7 @@ open Context.Rel.Declaration (* Ugly things which should not be here *) -let coq_constant m s = EConstr.of_constr @@ Universes.constr_of_global @@ +let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_global @@ Coqlib.coq_reference "RecursiveDefinition" m s let arith_Nat = ["Arith";"PeanoNat";"Nat"] @@ -61,7 +61,7 @@ let pr_leconstr_rd = let coq_init_constant s = EConstr.of_constr ( - Universes.constr_of_global @@ + UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s) let find_reference sl s = @@ -1241,7 +1241,7 @@ let get_current_subgoals_types () = exception EmptySubgoals let build_and_l sigma l = - let and_constr = Universes.constr_of_global @@ Coqlib.build_coq_and () in + let and_constr = UnivGen.constr_of_global @@ Coqlib.build_coq_and () in let conj_constr = coq_conj () in let mk_and p1 p2 = mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 168105e8f..4c0357dd8 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -373,7 +373,7 @@ struct * ZMicromega.v *) - let gen_constant_in_modules s m n = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules s m n) + let gen_constant_in_modules s m n = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules s m n) let init_constant = gen_constant_in_modules "ZMicromega" Coqlib.init_modules let constant = gen_constant_in_modules "ZMicromega" coq_modules let bin_constant = gen_constant_in_modules "ZMicromega" bin_module diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 81b44ffad..d2d4639d2 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -136,7 +136,7 @@ let mul = function | (Const n,q) when eq_num n num_1 -> q | (p,q) -> Mul(p,q) -let gen_constant msg path s = Universes.constr_of_global @@ +let gen_constant msg path s = UnivGen.constr_of_global @@ coq_reference msg path s let tpexpr = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PExpr") diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 51cd665f6..e455ebb28 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -206,7 +206,7 @@ let coq_modules = init_modules @arith_modules @ [logic_dir] @ zarith_base_modules @ [["Coq"; "omega"; "OmegaLemmas"]] -let gen_constant_in_modules n m s = EConstr.of_constr (Universes.constr_of_global @@ gen_reference_in_modules n m s) +let gen_constant_in_modules n m s = EConstr.of_constr (UnivGen.constr_of_global @@ gen_reference_in_modules n m s) let init_constant = gen_constant_in_modules "Omega" init_modules let constant = gen_constant_in_modules "Omega" coq_modules diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 912429c31..7464b42dc 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -120,7 +120,7 @@ open Proofview.Notations the constants are loaded in the environment *) let constant dir s = - EConstr.of_constr @@ Universes.constr_of_global @@ + EConstr.of_constr @@ UnivGen.constr_of_global @@ Coqlib.coq_reference "Quote" ("quote"::dir) s let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm") diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index ad3afafd8..949cba2db 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -69,19 +69,19 @@ let z_module = [["Coq";"ZArith";"BinInt"]] let init_constant x = EConstr.of_constr @@ - Universes.constr_of_global @@ + UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" Coqlib.init_modules x let constant x = EConstr.of_constr @@ - Universes.constr_of_global @@ + UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" coq_modules x let z_constant x = EConstr.of_constr @@ - Universes.constr_of_global @@ + UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" z_module x let bin_constant x = EConstr.of_constr @@ - Universes.constr_of_global @@ + UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" bin_module x (* Logic *) @@ -170,7 +170,7 @@ let mk_list univ typ l = loop l let mk_plist = - let type1lev = Universes.new_univ_level () in + let type1lev = UnivGen.new_univ_level () in fun l -> mk_list type1lev EConstr.mkProp l let mk_list = mk_list Univ.Level.set diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 946b6dff4..8a0f48dc4 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -26,27 +26,27 @@ let step_count = ref 0 let node_count = ref 0 -let logic_constant s = Universes.constr_of_global @@ +let logic_constant s = UnivGen.constr_of_global @@ Coqlib.coq_reference "refl_tauto" ["Init";"Logic"] s let li_False = lazy (destInd (logic_constant "False")) let li_and = lazy (destInd (logic_constant "and")) let li_or = lazy (destInd (logic_constant "or")) -let pos_constant s = Universes.constr_of_global @@ +let pos_constant s = UnivGen.constr_of_global @@ Coqlib.coq_reference "refl_tauto" ["Numbers";"BinNums"] s let l_xI = lazy (pos_constant "xI") let l_xO = lazy (pos_constant "xO") let l_xH = lazy (pos_constant "xH") -let store_constant s = Universes.constr_of_global @@ +let store_constant s = UnivGen.constr_of_global @@ Coqlib.coq_reference "refl_tauto" ["rtauto";"Bintree"] s let l_empty = lazy (store_constant "empty") let l_push = lazy (store_constant "push") -let constant s = Universes.constr_of_global @@ +let constant s = UnivGen.constr_of_global @@ Coqlib.coq_reference "refl_tauto" ["rtauto";"Rtauto"] s let l_Reflect = lazy (constant "Reflect") diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 074fcb92e..59ba4b7de 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -105,7 +105,7 @@ let protect_tac_in map id = let closed_term t l = let open Quote_plugin in Proofview.tclEVARMAP >>= fun sigma -> - let l = List.map Universes.constr_of_global l in + let l = List.map UnivGen.constr_of_global l in let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in if Quote.closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt()) @@ -233,7 +233,7 @@ let stdlib_modules = ] let coq_constant c = - lazy (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" stdlib_modules c)) + lazy (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" stdlib_modules c)) let coq_reference c = lazy (Coqlib.gen_reference_in_modules "Ring" stdlib_modules c) @@ -279,7 +279,7 @@ let plugin_modules = ] let my_constant c = - lazy (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c)) + lazy (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c)) let my_reference c = lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c) @@ -927,7 +927,7 @@ let ftheory_to_obj : field_info -> obj = let field_equality evd r inv req = match EConstr.kind !evd req with | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) -> - let c = Universes.constr_of_global (Coqlib.build_coq_eq_data()).congr in + let c = UnivGen.constr_of_global (Coqlib.build_coq_eq_data()).congr in let c = EConstr.of_constr c in mkApp(c,[|r;r;inv|]) | _ -> diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index e9e045a53..c0026616d 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1221,7 +1221,7 @@ let genclrtac cl cs clr = (fun type_err gl -> tclTHEN (tclTHEN (Proofview.V82.of_tactic (Tactics.elim_type (EConstr.of_constr - (Universes.constr_of_global @@ Coqlib.build_coq_False ())))) (old_cleartac clr)) + (UnivGen.constr_of_global @@ Coqlib.build_coq_False ())))) (old_cleartac clr)) (fun gl -> raise type_err) gl)) (old_cleartac clr) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 7d7655d29..a31022919 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -435,7 +435,7 @@ let lz_setoid_relation = | env', srel when env' == env -> srel | _ -> let srel = - try Some (Universes.constr_of_global @@ + try Some (UnivGen.constr_of_global @@ Coqlib.coq_reference "Class_setoid" sdir "RewriteRelation") with _ -> None in last_srel := (env, srel); srel @@ -482,7 +482,7 @@ let rwprocess_rule dir rule gl = | _ -> let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in EConstr.mkApp (pi2, ra), sigma in - if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_True ())) then + if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_True ())) then let s, sigma = sr sigma 2 in loop (converse_dir d) sigma s a.(1) rs 0 else diff --git a/pretyping/classops.ml b/pretyping/classops.ml index afa8a12fc..7dbef01c2 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -316,7 +316,7 @@ let lookup_pattern_path_between env (s,t) = let coercion_value { coe_value = c; coe_type = t; coe_context = ctx; coe_is_identity = b; coe_is_projection = b' } = - let subst, ctx = Universes.fresh_universe_context_set_instance ctx in + let subst, ctx = UnivGen.fresh_universe_context_set_instance ctx in let c' = Vars.subst_univs_level_constr subst c and t' = Vars.subst_univs_level_constr subst t in (make_judge (EConstr.of_constr c') (EConstr.of_constr t'), b, b'), ctx @@ -440,7 +440,7 @@ let cache_coercion env sigma (_, c) = let () = add_class c.coercion_target in let is, _ = class_info c.coercion_source in let it, _ = class_info c.coercion_target in - let value, ctx = Universes.fresh_global_instance env c.coercion_type in + let value, ctx = UnivGen.fresh_global_instance env c.coercion_type in let typ = Retyping.get_type_of env sigma (EConstr.of_constr value) in let typ = EConstr.Unsafe.to_constr typ in let xf = diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 49c429458..062136ff5 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -49,7 +49,7 @@ let _ = Goptions.declare_bool_option { (* XXX: we would like to search for this with late binding "data.id.type" etc... *) let impossible_default_case () = - let c, ctx = Universes.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in + let c, ctx = UnivGen.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in let (_, u) = Constr.destConst c in Some (c, Constr.mkConstU (Coqlib.type_of_id, u), ctx) @@ -210,7 +210,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = else match (Stack.strip_n_app (l_us-1) sk2_effective) with | None -> raise Not_found | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in - let u, ctx' = Universes.fresh_instance_from ctx None in + let u, ctx' = UnivGen.fresh_instance_from ctx None in let subst = Univ.make_inverse_instance_subst u in let c = EConstr.of_constr c in let c' = subst_univs_level_constr subst c in diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 3327c250d..40f4d4ff8 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -86,7 +86,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = if not (Sorts.List.mem kind (elim_sorts specif)) then raise (RecursionSchemeError - (NotAllowedCaseAnalysis (false, fst (Universes.fresh_sort_in_family env kind), pind))) + (NotAllowedCaseAnalysis (false, fst (UnivGen.fresh_sort_in_family env kind), pind))) in let ndepar = mip.mind_nrealdecls + 1 in @@ -550,7 +550,7 @@ let check_arities env listdepkind = let kelim = elim_sorts (mibi,mipi) in if not (Sorts.List.mem kind kelim) then raise (RecursionSchemeError - (NotAllowedCaseAnalysis (true, fst (Universes.fresh_sort_in_family env + (NotAllowedCaseAnalysis (true, fst (UnivGen.fresh_sort_in_family env kind),(mind,u)))) else if Int.List.mem ni ln then raise (RecursionSchemeError (NotMutualInScheme (mind,mind))) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index a4d447902..7394ad826 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -83,7 +83,7 @@ let declare_reduction_effect funkey f = (** A function to set the value of the print function *) let set_reduction_effect x funkey = - let termkey = Universes.constr_of_global x in + let termkey = UnivGen.constr_of_global x in Lib.add_anonymous_leaf (inReductionEffect (termkey,funkey)) @@ -705,7 +705,7 @@ let magicaly_constant_of_fixbody env sigma reference bd = function try let (cst_mod,cst_sect,_) = Constant.repr3 reference in let cst = Constant.make3 cst_mod cst_sect (Label.of_id id) in - let (cst, u), ctx = fresh_constant_instance env cst in + let (cst, u), ctx = UnivGen.fresh_constant_instance env cst in match constant_opt_value_in env (cst,u) with | None -> bd | Some t -> diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 4386144fe..11cc6c1f0 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -281,7 +281,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i)) in let ty, ctx = Global.type_of_global_in_context env glob in - let inst, ctx = Universes.fresh_instance_from ctx None in + let inst, ctx = UnivGen.fresh_instance_from ctx None in let ty = Vars.subst_instance_constr inst ty in let ty = EConstr.of_constr ty in let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in @@ -321,7 +321,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = hints @ (path', info, body) :: rest in List.fold_left declare_proj [] projs in - let term = Universes.constr_of_global_univ (glob, inst) in + let term = UnivGen.constr_of_global_univ (glob, inst) in (*FIXME subclasses should now get substituted for each particular instance of the polymorphic superclass *) aux pri term ty [glob] diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index c1d69dfc5..092bb5c27 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -75,7 +75,7 @@ let pf_ids_set_of_hyps gls = let pf_get_new_id id gls = next_ident_away id (pf_ids_set_of_hyps gls) -let pf_global gls id = EConstr.of_constr (Universes.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id)) +let pf_global gls id = EConstr.of_constr (UnivGen.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id)) let pf_reduction_of_red_expr gls re c = let (redfun, _) = reduction_of_red_expr (pf_env gls) re in diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index b3e1500ae..38fd817da 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -60,7 +60,7 @@ module Make(T : Task) () = struct type request = Request of T.request type more_data = - | MoreDataUnivLevel of Universes.universe_id list + | MoreDataUnivLevel of UnivGen.universe_id list let slave_respond (Request r) = let res = T.perform r in @@ -171,7 +171,7 @@ module Make(T : Task) () = struct | Unix.WSIGNALED sno -> Printf.sprintf "signalled(%d)" sno | Unix.WSTOPPED sno -> Printf.sprintf "stopped(%d)" sno) in let more_univs n = - CList.init n (fun _ -> Universes.new_univ_id ()) in + CList.init n (fun _ -> UnivGen.new_univ_id ()) in let rec kill_if () = if not (Worker.is_alive proc) then () @@ -310,7 +310,7 @@ module Make(T : Task) () = struct Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc in ignore (Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x)); (* We ask master to allocate universe identifiers *) - Universes.set_remote_new_univ_id (bufferize (fun () -> + UnivGen.set_remote_new_univ_id (bufferize (fun () -> marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel; match unmarshal_more_data (Option.get !slave_ic) with | MoreDataUnivLevel l -> l)); diff --git a/tactics/auto.ml b/tactics/auto.ml index 15a24fb37..77fe31415 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -79,7 +79,7 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl = let clenv, c = if poly then (** Refresh the instance of the hint *) - let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in + let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in let emap c = Vars.subst_univs_level_constr subst c in let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in (** Only metas are mentioning the old universes. *) diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index c3857e6b8..627ac31f5 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -93,7 +93,7 @@ let one_base general_rewrite_maybe_in tac_main bas = let try_rewrite dir ctx c tc = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in + let subst, ctx' = UnivGen.fresh_universe_context_set_instance ctx in let c' = Vars.subst_univs_level_constr subst c in let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index bbcf8def6..ea5d4719c 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -226,7 +226,7 @@ let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) = Refine.refine ~typecheck:false begin fun sigma -> let sigma, term, ty = if poly then - let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in + let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in let map c = Vars.subst_univs_level_constr subst c in let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in sigma, map c, map t diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 2408b8f2b..3df9e3f82 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -89,7 +89,7 @@ let rec prolog l n gl = let out_term env = function | IsConstr (c, _) -> c - | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance env gr)) + | IsGlobRef gr -> EConstr.of_constr (fst (UnivGen.fresh_global_instance env gr)) let prolog_tac l n = Proofview.V82.tactic begin fun gl -> diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 477de6452..715686ad0 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -102,7 +102,7 @@ let get_coq_eq ctx = let eq = Globnames.destIndRef Coqlib.glob_eq in (* Do not force the lazy if they are not defined *) let eq, ctx = with_context_set ctx - (Universes.fresh_inductive_instance (Global.env ()) eq) in + (UnivGen.fresh_inductive_instance (Global.env ()) eq) in mkIndU eq, mkConstructUi (eq,1), ctx with Not_found -> user_err Pp.(str "eq not found.") @@ -192,7 +192,7 @@ let get_non_sym_eq_data env (ind,u) = (**********************************************************************) let build_sym_scheme env ind = - let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in + let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = get_sym_eq_data env indu in let cstr n = @@ -241,11 +241,11 @@ let sym_scheme_kind = let const_of_scheme kind env ind ctx = let sym_scheme, eff = (find_scheme kind ind) in let sym, ctx = with_context_set ctx - (Universes.fresh_constant_instance (Global.env()) sym_scheme) in + (UnivGen.fresh_constant_instance (Global.env()) sym_scheme) in mkConstU sym, ctx, eff let build_sym_involutive_scheme env ind = - let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in + let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = get_sym_eq_data env indu in let eq,eqrefl,ctx = get_coq_eq ctx in @@ -353,7 +353,7 @@ let sym_involutive_scheme_kind = (**********************************************************************) let build_l2r_rew_scheme dep env ind kind = - let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in + let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = get_sym_eq_data env indu in let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in @@ -392,7 +392,7 @@ let build_l2r_rew_scheme dep env ind kind = rel_vect (nrealargs+4) nrealargs; rel_vect 1 nrealargs; [|mkRel 1|]]) in - let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in + let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in let ctx = Univ.ContextSet.union ctx ctx' in let s = mkSort s in let ci = make_case_info (Global.env()) ind RegularStyle in @@ -469,7 +469,7 @@ let build_l2r_rew_scheme dep env ind kind = (**********************************************************************) let build_l2r_forward_rew_scheme dep env ind kind = - let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in + let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = get_sym_eq_data env indu in let cstr n p = @@ -495,7 +495,7 @@ let build_l2r_forward_rew_scheme dep env ind kind = name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in let realsign_ind_P n aP = name_context env ((LocalAssum (Name varH,aP))::realsign_P n) in - let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in + let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in let ctx = Univ.ContextSet.union ctx ctx' in let s = mkSort s in let ci = make_case_info (Global.env()) ind RegularStyle in @@ -561,7 +561,7 @@ let build_l2r_forward_rew_scheme dep env ind kind = (**********************************************************************) let build_r2l_forward_rew_scheme dep env ind kind = - let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in + let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs) = get_non_sym_eq_data env indu in let cstr n = @@ -573,7 +573,7 @@ let build_r2l_forward_rew_scheme dep env ind kind = let applied_ind = build_dependent_inductive indu specif in let realsign_ind = name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in - let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in + let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in let ctx = Univ.ContextSet.union ctx ctx' in let s = mkSort s in let ci = make_case_info (Global.env()) ind RegularStyle in @@ -755,7 +755,7 @@ let rew_r2l_scheme_kind = let build_congr env (eq,refl,ctx) ind = let (ind,u as indu), ctx = with_context_set ctx - (Universes.fresh_inductive_instance env ind) in + (UnivGen.fresh_inductive_instance env ind) in let (mib,mip) = lookup_mind_specif env ind in if not (Int.equal (Array.length mib.mind_packets) 1) || not (Int.equal (Array.length mip.mind_nf_lc) 1) then error "Not an inductive type with a single constructor."; @@ -778,7 +778,7 @@ let build_congr env (eq,refl,ctx) ind = let varH = fresh env (Id.of_string "H") in let varf = fresh env (Id.of_string "f") in let ci = make_case_info (Global.env()) ind RegularStyle in - let uni, ctx = Universes.extend_context (Universes.new_global_univ ()) ctx in + let uni, ctx = UnivGen.extend_context (UnivGen.new_global_univ ()) ctx in let ctx = (fst ctx, Univ.enforce_leq uni (univ_of_eq env eq) (snd ctx)) in let c = my_it_mkLambda_or_LetIn paramsctxt diff --git a/tactics/equality.ml b/tactics/equality.ml index d142e10a4..8904cd170 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1781,7 +1781,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = try let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in let u = EInstance.kind sigma u in - let eq = Universes.constr_of_global_univ (lbeq.eq,u) in + let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; match EConstr.kind sigma x, EConstr.kind sigma y with | Var z, _ when not (is_evaluable env (EvalVarRef z)) -> @@ -1832,7 +1832,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = try let lbeq,u,(_,x,y) = find_eq_data_decompose c in let u = EInstance.kind sigma u in - let eq = Universes.constr_of_global_univ (lbeq.eq,u) in + let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; (* J.F.: added to prevent failure on goal containing x=x as an hyp *) if EConstr.eq_constr sigma x y then failwith "caught"; diff --git a/tactics/hints.ml b/tactics/hints.ml index d02bab186..39034a19b 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -876,7 +876,7 @@ let fresh_global_or_constr env sigma poly cr = let isgr, (c, ctx) = match cr with | IsGlobRef gr -> - let (c, ctx) = Universes.fresh_global_instance env gr in + let (c, ctx) = UnivGen.fresh_global_instance env gr in true, (EConstr.of_constr c, ctx) | IsConstr (c, ctx) -> false, (c, ctx) in diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 5e602289b..2a41a50dd 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -59,15 +59,15 @@ exception NonSingletonProp of inductive exception DecidabilityMutualNotSupported exception NoDecidabilityCoInductive -let constr_of_global g = lazy (Universes.constr_of_global g) +let constr_of_global g = lazy (UnivGen.constr_of_global g) (* Some pre declaration of constant we are going to use *) let bb = constr_of_global Coqlib.glob_bool -let andb_prop = fun _ -> Universes.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_prop +let andb_prop = fun _ -> UnivGen.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_prop let andb_true_intro = fun _ -> - Universes.constr_of_global + UnivGen.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_true_intro let tt = constr_of_global Coqlib.glob_true @@ -76,9 +76,9 @@ let ff = constr_of_global Coqlib.glob_false let eq = constr_of_global Coqlib.glob_eq -let sumbool () = Universes.constr_of_global (Coqlib.build_coq_sumbool ()) +let sumbool () = UnivGen.constr_of_global (Coqlib.build_coq_sumbool ()) -let andb = fun _ -> Universes.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb +let andb = fun _ -> UnivGen.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb let induct_on c = induction false None c None None @@ -863,7 +863,7 @@ let compute_dec_goal ind lnamesparrec nparrec = create_input ( mkNamedProd n (mkFullInd ind (2*nparrec)) ( mkNamedProd m (mkFullInd ind (2*nparrec+1)) ( - mkApp(sumbool(),[|eqnm;mkApp (Universes.constr_of_global @@ Coqlib.build_coq_not(),[|eqnm|])|]) + mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_global @@ Coqlib.build_coq_not(),[|eqnm|])|]) ) ) ) diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 26a46a752..722f21171 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -174,7 +174,7 @@ let do_assumptions kind nl l = let t = replace_vars subst t in let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in let subst' = List.map2 - (fun {CAst.v=id} (c,u) -> (id, Universes.constr_of_global_univ (c,u))) + (fun {CAst.v=id} (c,u) -> (id, UnivGen.constr_of_global_univ (c,u))) idl refs in subst'@subst, status' && status, next_uctx uctx) diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 32885ab88..2deca1e06 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -380,7 +380,7 @@ let do_mutual_induction_scheme lnamedepindsort = match inst with | None -> let _, ctx = Global.type_of_global_in_context env0 (IndRef ind) in - let u, ctx = Universes.fresh_instance_from ctx None in + let u, ctx = UnivGen.fresh_instance_from ctx None in let evd = Evd.from_ctx (UState.of_context_set ctx) in evd, (ind,u), Some u | Some ui -> evd, (ind, ui), inst diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 6de8539d4..624edeffe 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -259,7 +259,7 @@ let eterm_obligations env name evm fs ?status t ty = let tactics_module = ["Program";"Tactics"] let safe_init_constant md name () = Coqlib.check_required_library ("Coq"::md); - Universes.constr_of_global (Coqlib.coq_reference "Obligations" md name) + UnivGen.constr_of_global (Coqlib.coq_reference "Obligations" md name) let hide_obligation = safe_init_constant tactics_module "obligation" let pperror cmd = CErrors.user_err ~hdr:"Program" cmd -- cgit v1.2.3