aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/impargs.ml6
-rw-r--r--interp/notation.ml6
-rw-r--r--library/global.mli5
-rw-r--r--plugins/extraction/table.ml4
-rw-r--r--plugins/funind/indfun_common.ml2
-rw-r--r--plugins/ssr/ssrvernac.mlg2
-rw-r--r--pretyping/classops.ml2
-rw-r--r--pretyping/typeclasses.ml4
-rw-r--r--printing/prettyp.ml6
-rw-r--r--tactics/hints.ml2
-rw-r--r--vernac/auto_ind_decl.ml2
-rw-r--r--vernac/class.ml4
-rw-r--r--vernac/classes.ml2
-rw-r--r--vernac/indschemes.ml2
-rw-r--r--vernac/record.ml15
-rw-r--r--vernac/search.ml2
-rw-r--r--vernac/vernacentries.ml6
17 files changed, 35 insertions, 37 deletions
diff --git a/interp/impargs.ml b/interp/impargs.ml
index ce33cb8731..d8582d856e 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -450,13 +450,13 @@ let compute_mib_implicits flags kn =
(Array.mapi (* No need to lift, arities contain no de Bruijn *)
(fun i mip ->
(** No need to care about constraints here *)
- let ty, _ = Global.type_of_global_in_context env (IndRef (kn,i)) in
+ let ty, _ = Typeops.type_of_global_in_context env (IndRef (kn,i)) in
Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty))
mib.mind_packets) in
let env_ar = Environ.push_rel_context ar env in
let imps_one_inductive i mip =
let ind = (kn,i) in
- let ar, _ = Global.type_of_global_in_context env (IndRef ind) in
+ let ar, _ = Typeops.type_of_global_in_context env (IndRef ind) in
((IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)),
Array.mapi (fun j c ->
(ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags c))
@@ -694,7 +694,7 @@ let declare_manual_implicits local ref ?enriching l =
let flags = !implicit_args in
let env = Global.env () in
let sigma = Evd.from_env env in
- let t, _ = Global.type_of_global_in_context env ref in
+ let t, _ = Typeops.type_of_global_in_context env ref in
let t = of_constr t in
let enriching = Option.default flags.auto enriching in
let autoimpls = compute_auto_implicits env sigma flags enriching t in
diff --git a/interp/notation.ml b/interp/notation.ml
index 6104ab16c7..db8ee5bc18 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1314,7 +1314,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) =
| ArgsScopeNoDischarge -> assert false
| ArgsScopeAuto ->
let env = Global.env () in (*FIXME?*)
- let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in
+ let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in
let scs,cls = compute_arguments_scope_full sigma typ in
(req,r,List.length scs,scs,cls)
| ArgsScopeManual ->
@@ -1322,7 +1322,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) =
for the extra parameters of the section. Discard the classes
of the manually given scopes to avoid further re-computations. *)
let env = Global.env () in (*FIXME?*)
- let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in
+ let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in
let l',cls = compute_arguments_scope_full sigma typ in
let l1 = List.firstn n l' in
let cls1 = List.firstn n cls in
@@ -1369,7 +1369,7 @@ let find_arguments_scope r =
let declare_ref_arguments_scope sigma ref =
let env = Global.env () in (* FIXME? *)
- let typ = EConstr.of_constr @@ fst @@ Global.type_of_global_in_context env ref in
+ let typ = EConstr.of_constr @@ fst @@ Typeops.type_of_global_in_context env ref in
let (scs,cls as o) = compute_arguments_scope_full sigma typ in
declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o
diff --git a/library/global.mli b/library/global.mli
index 0c59330f6e..42a8005a4f 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -133,10 +133,7 @@ val constr_of_global_in_context : Environ.env ->
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
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 7b4fd280bd..f6eea3c5c4 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -446,7 +446,7 @@ let error_MPfile_as_mod mp b =
let argnames_of_global r =
let env = Global.env () in
- let typ, _ = Global.type_of_global_in_context env r in
+ let typ, _ = Typeops.type_of_global_in_context env r in
let rels,_ =
decompose_prod (Reduction.whd_all env typ) in
List.rev_map fst rels
@@ -878,7 +878,7 @@ let extract_constant_inline inline r ids s =
match g with
| ConstRef kn ->
let env = Global.env () in
- let typ, _ = Global.type_of_global_in_context env (ConstRef kn) in
+ let typ, _ = Typeops.type_of_global_in_context env (ConstRef kn) in
let typ = Reduction.whd_all env typ in
if Reduction.is_arity env typ
then begin
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index a385a61ae0..28a9542167 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -311,7 +311,7 @@ let pr_info f_info =
str "function_constant_type := " ++
(try
Printer.pr_lconstr_env env sigma
- (fst (Global.type_of_global_in_context env (ConstRef f_info.function_constant)))
+ (fst (Typeops.type_of_global_in_context env (ConstRef f_info.function_constant)))
with e when CErrors.noncritical e -> mt ()) ++ fnl () ++
str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 876751911b..940defb743 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -360,7 +360,7 @@ let coerce_search_pattern_to_sort hpat =
Pattern.PApp (fp, args') in
let hr, na = splay_search_pattern 0 hpat in
let dc, ht =
- let hr, _ = Global.type_of_global_in_context (Global.env ()) hr (** FIXME *) in
+ let hr, _ = Typeops.type_of_global_in_context 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
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index b026397abf..543eea59c1 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -380,7 +380,7 @@ type coercion = {
(* Computation of the class arity *)
let reference_arity_length ref =
- let t, _ = Global.type_of_global_in_context (Global.env ()) ref in
+ let t, _ = Typeops.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/typeclasses.ml b/pretyping/typeclasses.ml
index ce12aaeeb0..0bc35e5358 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -279,7 +279,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
(fun () -> incr i;
Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i))
in
- let ty, ctx = Global.type_of_global_in_context env glob in
+ let ty, ctx = Typeops.type_of_global_in_context env glob 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
@@ -420,7 +420,7 @@ let remove_instance i =
remove_instance_hint i.is_impl
let declare_instance info local glob =
- let ty, _ = Global.type_of_global_in_context (Global.env ()) glob in
+ let ty, _ = Typeops.type_of_global_in_context (Global.env ()) glob in
let info = Option.default {hint_priority = None; hint_pattern = None} info in
match class_of_constr Evd.empty (EConstr.of_constr ty) with
| Some (rels, ((tc,_), args) as _cl) ->
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index e6f82c60ee..4619e049e0 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -71,7 +71,7 @@ let int_or_no n = if Int.equal n 0 then str "no" else int n
let print_basename sp = pr_global (ConstRef sp)
let print_ref reduce ref udecl =
- let typ, univs = Global.type_of_global_in_context (Global.env ()) ref in
+ let typ, univs = Typeops.type_of_global_in_context (Global.env ()) ref in
let inst = Univ.make_abstract_instance univs in
let bl = UnivNames.universe_binders_with_opt_names ref udecl in
let sigma = Evd.from_ctx (UState.of_binders bl) in
@@ -147,7 +147,7 @@ let print_renames_list prefix l =
hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map Name.print l))]
let need_expansion impl ref =
- let typ, _ = Global.type_of_global_in_context (Global.env ()) ref in
+ let typ, _ = Typeops.type_of_global_in_context (Global.env ()) ref in
let ctx = Term.prod_assum typ in
let nprods = List.count is_local_assum ctx in
not (List.is_empty impl) && List.length impl >= nprods &&
@@ -823,7 +823,7 @@ let print_opaque_name env sigma qid =
| IndRef (sp,_) ->
print_inductive sp None
| ConstructRef cstr as gr ->
- let ty, ctx = Global.type_of_global_in_context env gr in
+ let ty, ctx = Typeops.type_of_global_in_context env gr in
let ty = EConstr.of_constr ty in
let open EConstr in
print_typed_value_in_env env sigma (mkConstruct cstr, ty)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 0c10f32c86..2f2d32e887 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -942,7 +942,7 @@ let make_extern pri pat tacast =
let make_mode ref m =
let open Term in
- let ty, _ = Global.type_of_global_in_context (Global.env ()) ref in
+ let ty, _ = Typeops.type_of_global_in_context (Global.env ()) ref in
let ctx, t = decompose_prod ty in
let n = List.length ctx in
let m' = Array.of_list m in
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 9f71def8fc..fa1b8eeb3e 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -113,7 +113,7 @@ let mkFullInd (ind,u) n =
else mkIndU (ind,u)
let check_bool_is_defined () =
- try let _ = Global.type_of_global_in_context (Global.env ()) Coqlib.(lib_ref "core.bool.type") in ()
+ try let _ = Typeops.type_of_global_in_context (Global.env ()) Coqlib.(lib_ref "core.bool.type") in ()
with e when CErrors.noncritical e -> raise (UndefinedCst "bool")
let check_no_indices mib =
diff --git a/vernac/class.ml b/vernac/class.ml
index 614b2181d9..62efc72f1f 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -66,7 +66,7 @@ let explain_coercion_error g = function
let check_reference_arity ref =
let env = Global.env () in
- let c, _ = Global.type_of_global_in_context env ref in
+ let c, _ = Typeops.type_of_global_in_context env ref in
if not (Reductionops.is_arity env (Evd.from_env env) (EConstr.of_constr c)) (** FIXME *) then
raise (CoercionError (NotAClass ref))
@@ -249,7 +249,7 @@ let warn_uniform_inheritance =
let add_new_coercion_core coef stre poly source target isid =
check_source source;
- let t, _ = Global.type_of_global_in_context (Global.env ()) coef in
+ let t, _ = Typeops.type_of_global_in_context (Global.env ()) coef in
if coercion_exists coef then raise (CoercionError AlreadyExists);
let lp,tg = decompose_prod_assum t in
let llp = List.length lp in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 3cf5e9bfdf..ca0387fd1b 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -70,7 +70,7 @@ let existing_instance glob g info =
let c = global g in
let info = Option.default Hints.empty_hint_info info in
let info = intern_info info in
- let instance, _ = Global.type_of_global_in_context (Global.env ()) c in
+ let instance, _ = Typeops.type_of_global_in_context (Global.env ()) c in
let _, r = Term.decompose_prod_assum instance in
match class_of_constr Evd.empty (EConstr.of_constr r) with
| Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob c)
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 5f2818c12b..8d691eb3b2 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -387,7 +387,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
let evd, indu, inst =
match inst with
| None ->
- let _, ctx = Global.type_of_global_in_context env0 (IndRef ind) in
+ let _, ctx = Typeops.type_of_global_in_context env0 (IndRef ind) 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
diff --git a/vernac/record.ml b/vernac/record.ml
index 724b6e62fe..3ba360fee4 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -574,8 +574,8 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
List.map map data
-let add_constant_class cst =
- let ty, univs = Global.type_of_global_in_context (Global.env ()) (ConstRef cst) in
+let add_constant_class env cst =
+ let ty, univs = Typeops.type_of_global_in_context env (ConstRef cst) in
let ctx, arity = decompose_prod_assum ty in
let tc =
{ cl_univs = univs;
@@ -589,12 +589,12 @@ let add_constant_class cst =
in add_class tc;
set_typeclass_transparency (EvalConstRef cst) false false
-let add_inductive_class ind =
- let mind, oneind = Global.lookup_inductive ind in
+let add_inductive_class env ind =
+ let mind, oneind = Inductive.lookup_mind_specif env ind in
let k =
let ctx = oneind.mind_arity_ctxt in
let univs = Declareops.inductive_polymorphic_context mind in
- let env = push_context ~strict:false (Univ.AUContext.repr univs) (Global.env ()) in
+ let env = push_context ~strict:false (Univ.AUContext.repr univs) env in
let env = push_rel_context ctx env in
let inst = Univ.make_abstract_instance univs in
let ty = Inductive.type_of_inductive env ((mind, oneind), inst) in
@@ -612,11 +612,12 @@ let warn_already_existing_class =
Printer.pr_global g ++ str " is already declared as a typeclass.")
let declare_existing_class g =
+ let env = Global.env () in
if Typeclasses.is_class g then warn_already_existing_class g
else
match g with
- | ConstRef x -> add_constant_class x
- | IndRef x -> add_inductive_class x
+ | ConstRef x -> add_constant_class env x
+ | IndRef x -> add_inductive_class env x
| _ -> user_err ~hdr:"declare_existing_class"
(Pp.str"Unsupported class type, only constants and inductives are allowed")
diff --git a/vernac/search.ml b/vernac/search.ml
index 04dcb7d565..23e53ce673 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -80,7 +80,7 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) =
| "CONSTANT" ->
let cst = Global.constant_of_delta_kn kn in
let gr = ConstRef cst in
- let (typ, _) = Global.type_of_global_in_context (Global.env ()) gr in
+ let (typ, _) = Typeops.type_of_global_in_context (Global.env ()) gr in
fn gr env typ
| "INDUCTIVE" ->
let mind = Global.mind_of_delta_kn kn in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 48d4165830..1190d73258 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1101,6 +1101,8 @@ let warn_arguments_assert =
[args] is the main list of arguments statuses,
[more_implicits] is a list of extra lists of implicit statuses *)
let vernac_arguments ~atts reference args more_implicits nargs_for_red flags =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
let assert_flag = List.mem `Assert flags in
let rename_flag = List.mem `Rename flags in
let clear_scopes_flag = List.mem `ClearScopes flags in
@@ -1125,9 +1127,7 @@ let vernac_arguments ~atts reference args more_implicits nargs_for_red flags =
let sr = smart_global reference in
let inf_names =
- let ty, _ = Global.type_of_global_in_context (Global.env ()) sr in
- let env = Global.env () in
- let sigma = Evd.from_env env in
+ let ty, _ = Typeops.type_of_global_in_context env sr in
Impargs.compute_implicits_names env sigma (EConstr.of_constr ty)
in
let prev_names =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:04:42 +0000