aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--API/API.mli4
-rw-r--r--engine/termops.ml2
-rw-r--r--engine/universes.ml66
-rw-r--r--engine/universes.mli11
-rw-r--r--library/global.ml19
-rw-r--r--library/global.mli7
-rw-r--r--plugins/funind/functional_principles_types.ml2
-rw-r--r--plugins/funind/recdef.ml2
-rw-r--r--plugins/ssr/ssrvernac.ml43
-rw-r--r--pretyping/classops.ml2
-rw-r--r--pretyping/pretyping.ml4
-rw-r--r--printing/prettyp.ml6
-rw-r--r--tactics/tactics.ml4
13 files changed, 43 insertions, 89 deletions
diff --git a/API/API.mli b/API/API.mli
index 0f3394fe9..f8fb96aa9 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2684,10 +2684,8 @@ sig
val fresh_inductive_instance : Environ.env -> Names.inductive -> Term.pinductive Univ.in_universe_context_set
val new_Type : Names.DirPath.t -> Term.types
val type_of_global : Globnames.global_reference -> Term.types Univ.in_universe_context_set
- val unsafe_type_of_global : Globnames.global_reference -> Term.types
val constr_of_global : Prelude.global_reference -> Term.constr
val new_univ_level : Names.DirPath.t -> Univ.Level.t
- val unsafe_constr_of_global : Globnames.global_reference -> Term.constr Univ.in_universe_context
val new_sort_in_family : Sorts.family -> Sorts.t
val pr_with_global_universes : Univ.Level.t -> Pp.std_ppcmds
val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds
@@ -2713,6 +2711,8 @@ sig
val env_of_context : Environ.named_context_val -> Environ.env
val is_polymorphic : Globnames.global_reference -> bool
+ val constr_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.t * Univ.AUContext.t
+ val type_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.t * Univ.AUContext.t
val type_of_global_unsafe : Globnames.global_reference -> Term.types
val current_dirpath : unit -> Names.DirPath.t
diff --git a/engine/termops.ml b/engine/termops.ml
index fc3291df1..1aba2bbdd 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -906,7 +906,7 @@ let collect_vars sigma c =
aux Id.Set.empty c
let vars_of_global_reference env gr =
- let c, _ = Universes.unsafe_constr_of_global gr in
+ let c, _ = Global.constr_of_global_in_context env gr in
vars_of_global (Global.env ()) c
(* Tests whether [m] is a subterm of [t]:
diff --git a/engine/universes.ml b/engine/universes.ml
index fc441fd0b..21854b3fa 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -319,9 +319,6 @@ let fresh_instance_from ctx inst =
let constraints = AUContext.instantiate inst ctx in
inst, (ctx', constraints)
-let unsafe_instance_from ctx =
- (Univ.AUContext.instance ctx, Univ.instantiate_univ_context ctx)
-
(** Fresh universe polymorphic construction *)
let fresh_constant_instance env c inst =
@@ -358,34 +355,6 @@ let fresh_constructor_instance env (ind,i) inst =
let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in
(((ind,i),inst), ctx)
-let unsafe_constant_instance env c =
- let cb = lookup_constant c env in
- match cb.Declarations.const_universes with
- | Declarations.Monomorphic_const _ ->
- ((c,Instance.empty), UContext.empty)
- | Declarations.Polymorphic_const auctx ->
- let inst, ctx = unsafe_instance_from auctx in ((c, inst), ctx)
-
-let unsafe_inductive_instance env ind =
- let mib, mip = Inductive.lookup_mind_specif env ind in
- match mib.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ -> ((ind,Instance.empty), UContext.empty)
- | Declarations.Polymorphic_ind auctx ->
- let inst, ctx = unsafe_instance_from auctx in ((ind,inst), ctx)
- | Declarations.Cumulative_ind acumi ->
- let inst, ctx = unsafe_instance_from (ACumulativityInfo.univ_context acumi) in
- ((ind,inst), ctx)
-
-let unsafe_constructor_instance env (ind,i) =
- let mib, mip = Inductive.lookup_mind_specif env ind in
- match mib.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ -> (((ind, i),Instance.empty), UContext.empty)
- | Declarations.Polymorphic_ind auctx ->
- let inst, ctx = unsafe_instance_from auctx in (((ind, i),inst), ctx)
- | Declarations.Cumulative_ind acumi ->
- let inst, ctx = unsafe_instance_from (ACumulativityInfo.univ_context acumi) in
- (((ind, i),inst), ctx)
-
open Globnames
let fresh_global_instance ?names env gr =
@@ -410,19 +379,6 @@ let fresh_inductive_instance env sp =
let fresh_constructor_instance env sp =
fresh_constructor_instance env sp None
-let unsafe_global_instance env gr =
- match gr with
- | VarRef id -> mkVar id, UContext.empty
- | ConstRef sp ->
- let c, ctx = unsafe_constant_instance env sp in
- mkConstU c, ctx
- | ConstructRef sp ->
- let c, ctx = unsafe_constructor_instance env sp in
- mkConstructU c, ctx
- | IndRef sp ->
- let c, ctx = unsafe_inductive_instance env sp in
- mkIndU c, ctx
-
let constr_of_global gr =
let c, ctx = fresh_global_instance (Global.env ()) gr in
if not (Univ.ContextSet.is_empty ctx) then
@@ -437,9 +393,6 @@ let constr_of_global gr =
let constr_of_reference = constr_of_global
-let unsafe_constr_of_global gr =
- unsafe_global_instance (Global.env ()) gr
-
let constr_of_global_univ (gr,u) =
match gr with
| VarRef id -> mkVar id
@@ -513,25 +466,6 @@ let type_of_reference env r =
let type_of_global t = type_of_reference (Global.env ()) t
-let unsafe_type_of_reference env r =
- match r with
- | VarRef id -> Environ.named_type id env
- | ConstRef c ->
- let cb = Environ.lookup_constant c env in
- Typeops.type_of_constant_type env cb.const_type
-
- | IndRef ind ->
- let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
- let (_, inst), _ = unsafe_inductive_instance env ind in
- Inductive.type_of_inductive env (specif, inst)
-
- | ConstructRef (ind, _ as cstr) ->
- let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
- let (_, inst), _ = unsafe_inductive_instance env ind in
- Inductive.type_of_constructor (cstr,inst) specif
-
-let unsafe_type_of_global t = unsafe_type_of_reference (Global.env ()) t
-
let fresh_sort_in_family env = function
| InProp -> prop_sort, ContextSet.empty
| InSet -> set_sort, ContextSet.empty
diff --git a/engine/universes.mli b/engine/universes.mli
index 5f4d212b6..8d0f106de 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -189,22 +189,11 @@ val constr_of_global : Globnames.global_reference -> constr
(** ** DEPRECATED ** synonym of [constr_of_global] *)
val constr_of_reference : Globnames.global_reference -> constr
-(** [unsafe_constr_of_global gr] turns [gr] into a constr, works on polymorphic
- references by taking the original universe instance that is not recorded
- anywhere. The constraints are forgotten as well. DO NOT USE in new code. *)
-val unsafe_constr_of_global : Globnames.global_reference -> constr in_universe_context
-
(** 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 : Globnames.global_reference -> types in_universe_context_set
-(** [unsafe_type_of_global gr] returns [gr]'s type, works on polymorphic
- references by taking the original universe instance that is not recorded
- anywhere. The constraints are forgotten as well.
- USE with care. *)
-val unsafe_type_of_global : Globnames.global_reference -> types
-
(** Full universes substitutions into terms *)
val nf_evars_and_universes_opt_subst : (existential -> constr option) ->
diff --git a/library/global.ml b/library/global.ml
index 3a74f535d..5fff26566 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -191,6 +191,25 @@ let type_of_global_unsafe r =
let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in
Inductive.type_of_constructor (cstr,inst) specif
+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
diff --git a/library/global.mli b/library/global.mli
index d6d2f1f85..0f1cec44a 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -122,6 +122,13 @@ val is_polymorphic : Globnames.global_reference -> bool
val is_template_polymorphic : Globnames.global_reference -> bool
val is_type_in_type : Globnames.global_reference -> bool
+val constr_of_global_in_context : Environ.env ->
+ Globnames.global_reference -> 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. *)
+
val type_of_global_in_context : Environ.env ->
Globnames.global_reference -> Constr.types * Univ.AUContext.t
(** Returns the type of the constant in its local universe
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 8c9b514e6..d726c1a2b 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -651,7 +651,7 @@ let build_case_scheme fa =
(* in *)
let funs =
let (_,f,_) = fa in
- try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
+ try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f))
with Not_found ->
user_err ~hdr:"FunInd.build_case_scheme"
(str "Cannot find " ++ Libnames.pr_reference f) in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 1705cac78..bc550c8b9 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -90,7 +90,7 @@ let type_of_const sigma t =
|_ -> assert false
let constr_of_global x =
- fst (Universes.unsafe_constr_of_global x)
+ fst (Global.constr_of_global_in_context (Global.env ()) x)
let constant sl s = constr_of_global (find_reference sl s)
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 4c8827bf8..cb6a2cd69 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -337,7 +337,8 @@ let coerce_search_pattern_to_sort hpat =
Pattern.PApp (fp, args') in
let hr, na = splay_search_pattern 0 hpat in
let dc, ht =
- Reductionops.splay_prod env sigma (EConstr.of_constr (Universes.unsafe_type_of_global hr)) in
+ let hr, _ = Global.type_of_global_in_context (Global.env ()) hr (** FIXME *) in
+ Reductionops.splay_prod env sigma (EConstr.of_constr hr) in
let np = List.length dc in
if np < na then CErrors.user_err (Pp.str "too many arguments in head search pattern") else
let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 948aa26ca..078990a8c 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -403,7 +403,7 @@ type coercion = {
(* Computation of the class arity *)
let reference_arity_length ref =
- let t = Universes.unsafe_type_of_global ref in
+ let t, _ = Global.type_of_global_in_context (Global.env ()) ref in
List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty (EConstr.of_constr t))) (** FIXME *)
let projection_arity_length p =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e166e0e9d..bfc6bf5cf 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -511,8 +511,8 @@ let pretype_global ?loc rigid env evd gr us =
match us with
| None -> evd, None
| Some l ->
- let _, ctx = Universes.unsafe_constr_of_global gr in
- let len = Univ.UContext.size ctx in
+ let _, ctx = Global.constr_of_global_in_context env.ExtraEnv.env gr in
+ let len = Univ.AUContext.size ctx in
interp_instance ?loc evd ~len l
in
let (sigma, c) = Evd.fresh_global ?loc ~rigid ?names:instance env.ExtraEnv.env evd gr in
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index d1e51c9f3..a0c88a7af 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -798,9 +798,11 @@ let print_opaque_name qid =
| IndRef (sp,_) ->
print_inductive sp
| ConstructRef cstr as gr ->
- let open EConstr in
- let ty = Universes.unsafe_type_of_global gr in
+ let ty, ctx = Global.type_of_global_in_context env gr in
+ let inst = Univ.AUContext.instance ctx in
+ let ty = Vars.subst_instance_constr inst ty in
let ty = EConstr.of_constr ty in
+ let open EConstr in
print_typed_value (mkConstruct cstr, ty)
| VarRef id ->
env |> lookup_named id |> NamedDecl.set_id id |> print_named_decl
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2e3a4e33b..177c44bcb 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5004,7 +5004,9 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
in
let cst = Impargs.with_implicit_protection cst () in
(* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *)
- let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in
+ let lem, ctx = Global.constr_of_global_in_context (Global.env ()) (ConstRef cst) in
+ let inst = Univ.AUContext.instance ctx in
+ let lem = CVars.subst_instance_constr inst lem in
let lem = EConstr.of_constr lem in
let evd = Evd.set_universe_context evd ectx in
let open Safe_typing in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 00:52:13 +0000