aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/cctac.ml2
-rw-r--r--plugins/extraction/extraction.ml2
-rw-r--r--plugins/firstorder/formula.ml8
-rw-r--r--plugins/firstorder/sequent.ml2
-rw-r--r--plugins/funind/glob_term_to_relation.ml6
-rw-r--r--plugins/funind/glob_termops.ml2
-rw-r--r--plugins/funind/indfun.ml4
-rw-r--r--plugins/ltac/rewrite.ml66
-rw-r--r--plugins/ltac/tacsubst.ml6
-rw-r--r--plugins/ltac/tauto.ml18
-rw-r--r--plugins/ssr/ssrelim.ml2
-rw-r--r--plugins/ssr/ssrequality.ml6
-rw-r--r--plugins/ssr/ssrview.ml2
13 files changed, 69 insertions, 57 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 50fc2448fc..0e3b9fc2b6 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -67,7 +67,7 @@ let rec decompose_term env sigma t=
let canon_mind = MutInd.make1 (MutInd.canonical mind) in
let canon_ind = canon_mind,i_ind in
let (oib,_)=Global.lookup_inductive (canon_ind) in
- let nargs=constructor_nallargs_env env (canon_ind,i_con) in
+ let nargs=constructor_nallargs env (canon_ind,i_con) in
Constructor {ci_constr= ((canon_ind,i_con),u);
ci_arity=nargs;
ci_nhyps=nargs-oib.mind_nparams}
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index c9cfd74362..9db7c8d8d3 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -854,7 +854,7 @@ and extract_cons_app env sg mle mlt (((kn,i) as ip,j) as cp) args =
and extract_case env sg mle ((kn,i) as ip,c,br) mlt =
(* [br]: bodies of each branch (in functional form) *)
(* [ni]: number of arguments without parameters in each branch *)
- let ni = constructors_nrealargs_env env ip in
+ let ni = constructors_nrealargs env ip in
let br_size = Array.length br in
assert (Int.equal (Array.length ni) br_size);
if Int.equal br_size 0 then begin
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 56b3dc97cf..4b7bc707d6 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -82,13 +82,13 @@ let pop t = Vars.lift (-1) t
let kind_of_formula env sigma term =
let normalize = special_nf env sigma in
let cciterm = special_whd env sigma term in
- match match_with_imp_term sigma cciterm with
+ match match_with_imp_term env sigma cciterm with
Some (a,b)-> Arrow (a, pop b)
|_->
- match match_with_forall_term sigma cciterm with
+ match match_with_forall_term env sigma cciterm with
Some (_,a,b)-> Forall (a, b)
|_->
- match match_with_nodep_ind sigma cciterm with
+ match match_with_nodep_ind env sigma cciterm with
Some (i,l,n)->
let ind,u=EConstr.destInd sigma i in
let u = EConstr.EInstance.kind sigma u in
@@ -111,7 +111,7 @@ let kind_of_formula env sigma term =
else
Or((ind,u),l,is_trivial)
| _ ->
- match match_with_sigma_type sigma cciterm with
+ match match_with_sigma_type env sigma cciterm with
Some (i,l)->
let (ind, u) = EConstr.destInd sigma i in
let u = EConstr.EInstance.kind sigma u in
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 01b18e2f30..9f2ceb2c28 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -188,7 +188,7 @@ let empty_seq depth=
let expand_constructor_hints =
List.map_append (function
| GlobRef.IndRef ind ->
- List.init (Inductiveops.nconstructors ind)
+ List.init (Inductiveops.nconstructors (Global.env()) ind)
(fun i -> GlobRef.ConstructRef (ind,i+1))
| gr ->
[gr])
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 275b58f0aa..45a4e61846 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -317,7 +317,7 @@ let build_constructors_of_type ind' argl =
Impargs.implicits_of_global constructref
in
let cst_narg =
- Inductiveops.constructor_nallargs_env
+ Inductiveops.constructor_nallargs
(Global.env ())
construct
in
@@ -330,7 +330,7 @@ let build_constructors_of_type ind' argl =
let pat_as_term =
mkGApp(mkGRef (ConstructRef(ind',i+1)),argl)
in
- cases_pattern_of_glob_constr Anonymous pat_as_term
+ cases_pattern_of_glob_constr (Global.env()) Anonymous pat_as_term
)
ind.Declarations.mind_consnames
@@ -415,7 +415,7 @@ let rec pattern_to_term_and_type env typ = DAst.with_val (function
mkGVar id
| PatCstr(constr,patternl,_) ->
let cst_narg =
- Inductiveops.constructor_nallargs_env
+ Inductiveops.constructor_nallargs
(Global.env ())
constr
in
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 13ff19a46b..7b758da8e8 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -361,7 +361,7 @@ let rec pattern_to_term pt = DAst.with_val (function
mkGVar id
| PatCstr(constr,patternl,_) ->
let cst_narg =
- Inductiveops.constructor_nallargs_env
+ Inductiveops.constructor_nallargs
(Global.env ())
constr
in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index a5c19f3217..e582362e25 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -382,8 +382,8 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
let _ =
List.map_i
(fun i x ->
- let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in
- let env = Global.env () in
+ let env = Global.env () in
+ let princ = Indrec.lookup_eliminator env (ind_kn,i) (InProp) in
let evd = ref (Evd.from_env env) in
let evd',uprinc = Evd.fresh_global env !evd princ in
let _ = evd := evd' in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 75565c1a34..2d40ba6562 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -119,7 +119,7 @@ let app_poly_check env evars f args =
(evars, cstrs), t
let app_poly_nocheck env evars f args =
- let evars, fc = f evars in
+ let evars, fc = f evars in
evars, mkApp (fc, args)
let app_poly_sort b =
@@ -175,25 +175,29 @@ end) = struct
let rewrite_relation_class = find_global relation_classes "RewriteRelation"
- let proper_class = lazy (class_info (find_reference morphisms "Proper"))
- let proper_proxy_class = lazy (class_info (find_reference morphisms "ProperProxy"))
-
- let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs))))
-
- let proper_type =
- let l = lazy (Lazy.force proper_class).cl_impl in
- fun (evd,cstrs) ->
- let (evd, c) = Evarutil.new_global evd (Lazy.force l) in
- (evd, cstrs), c
-
- let proper_proxy_type =
- let l = lazy (Lazy.force proper_proxy_class).cl_impl in
- fun (evd,cstrs) ->
- let (evd, c) = Evarutil.new_global evd (Lazy.force l) in
- (evd, cstrs), c
+ let proper_class =
+ let r = lazy (find_reference morphisms "Proper") in
+ fun env sigma -> class_info env sigma (Lazy.force r)
+
+ let proper_proxy_class =
+ let r = lazy (find_reference morphisms "ProperProxy") in
+ fun env sigma -> class_info env sigma (Lazy.force r)
+
+ let proper_proj env sigma =
+ mkConst (Option.get (pi3 (List.hd (proper_class env sigma).cl_projs)))
+
+ let proper_type env (sigma,cstrs) =
+ let l = (proper_class env sigma).cl_impl in
+ let (sigma, c) = Evarutil.new_global sigma l in
+ (sigma, cstrs), c
+
+ let proper_proxy_type env (sigma,cstrs) =
+ let l = (proper_proxy_class env sigma).cl_impl in
+ let (sigma, c) = Evarutil.new_global sigma l in
+ (sigma, cstrs), c
let proper_proof env evars carrier relation x =
- let evars, goal = app_poly env evars proper_proxy_type [| carrier ; relation; x |] in
+ let evars, goal = app_poly env evars (proper_proxy_type env) [| carrier ; relation; x |] in
new_cstr_evar evars env goal
let get_reflexive_proof env = find_class_proof reflexive_type reflexive_proof env
@@ -800,7 +804,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
in
(* Actual signature found *)
let cl_args = [| appmtype' ; signature ; appm |] in
- let evars, app = app_poly_sort b env evars (if b then PropGlobal.proper_type else TypeGlobal.proper_type)
+ let evars, app = app_poly_sort b env evars (if b then PropGlobal.proper_type env else TypeGlobal.proper_type env)
cl_args in
let env' =
let dosub, appsub =
@@ -1310,8 +1314,8 @@ module Strategies =
in
let evars, proof =
let proxy =
- if prop then PropGlobal.proper_proxy_type
- else TypeGlobal.proper_proxy_type
+ if prop then PropGlobal.proper_proxy_type env
+ else TypeGlobal.proper_proxy_type env
in
let evars, mty = app_poly_sort prop env evars proxy [| ty ; rel; t |] in
new_cstr_evar evars env mty
@@ -1854,12 +1858,12 @@ let declare_relation ~pstate atts ?(binders=[]) a aeq n refl symm trans =
let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None)
-let proper_projection sigma r ty =
+let proper_projection env sigma r ty =
let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in
let ctx, inst = decompose_prod_assum sigma ty in
let mor, args = destApp sigma inst in
let instarg = mkApp (r, rel_vect 0 (List.length ctx)) in
- let app = mkApp (Lazy.force PropGlobal.proper_proj,
+ let app = mkApp (PropGlobal.proper_proj env sigma,
Array.append args [| instarg |]) in
it_mkLambda_or_LetIn app ctx
@@ -1869,7 +1873,7 @@ let declare_projection n instance_id r =
let sigma = Evd.from_env env in
let sigma,c = Evd.fresh_global env sigma r in
let ty = Retyping.get_type_of env sigma c in
- let term = proper_projection sigma c ty in
+ let term = proper_projection env sigma c ty in
let sigma, typ = Typing.type_of env sigma term in
let ctx, typ = decompose_prod_assum sigma typ in
let typ =
@@ -1924,7 +1928,7 @@ let build_morphism_signature env sigma m =
rel)
cstrs
in
- let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in
+ let morph = e_app_poly env evd (PropGlobal.proper_type env) [| t; sig_; m |] in
let evd = solve_constraints env !evd in
let evd = Evd.minimize_universes evd in
let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in
@@ -1938,9 +1942,9 @@ let default_morphism sign m =
let evars, _, sign, cstrs =
PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign)
in
- let evars, morph = app_poly_check env evars PropGlobal.proper_type [| t; sign; m |] in
+ let evars, morph = app_poly_check env evars (PropGlobal.proper_type env) [| t; sign; m |] in
let evars, mor = resolve_one_typeclass env (goalevars evars) morph in
- mor, proper_projection sigma mor morph
+ mor, proper_projection env sigma mor morph
let warn_add_setoid_deprecated =
CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () ->
@@ -1984,8 +1988,8 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option =
(None,(instance,uctx),None),
Decl_kinds.IsAssumption Decl_kinds.Logical)
in
- add_instance (Typeclasses.new_instance
- (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info atts.global (ConstRef cst));
+ add_instance (Classes.mk_instance
+ (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
declare_projection n instance_id (ConstRef cst);
pstate
else
@@ -1995,8 +1999,8 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option =
let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
let hook _ _ _ = function
| Globnames.ConstRef cst ->
- add_instance (Typeclasses.new_instance
- (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
+ add_instance (Classes.mk_instance
+ (PropGlobal.proper_class env evd) Hints.empty_hint_info
atts.global (ConstRef cst));
declare_projection n instance_id (ConstRef cst)
| _ -> assert false
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index caaa547a07..e617f3d45e 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -30,7 +30,7 @@ let subst_quantified_hypothesis _ x = x
let subst_declared_or_quantified_hypothesis _ x = x
let subst_glob_constr_and_expr subst (c, e) =
- (Detyping.subst_glob_constr subst c, e)
+ (Detyping.subst_glob_constr (Global.env()) subst c, e)
let subst_glob_constr = subst_glob_constr_and_expr (* shortening *)
@@ -99,7 +99,9 @@ let subst_evaluable subst =
let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c)
let subst_glob_constr_or_pattern subst (bvars,c,p) =
- (bvars,subst_glob_constr subst c,subst_pattern subst p)
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ (bvars,subst_glob_constr subst c,subst_pattern env sigma subst p)
let subst_redexp subst =
Redops.map_red_expr_gen
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 4c65445b89..d1951cc18d 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -98,16 +98,18 @@ let split = Tactics.split_with_bindings false [Tactypes.NoBindings]
(** Test *)
let is_empty _ ist =
+ Proofview.tclENV >>= fun genv ->
Proofview.tclEVARMAP >>= fun sigma ->
- if is_empty_type sigma (assoc_var "X1" ist) then idtac else fail
+ if is_empty_type genv sigma (assoc_var "X1" ist) then idtac else fail
(* Strictly speaking, this exceeds the propositional fragment as it
matches also equality types (and solves them if a reflexivity) *)
let is_unit_or_eq _ ist =
+ Proofview.tclENV >>= fun genv ->
Proofview.tclEVARMAP >>= fun sigma ->
let flags = assoc_flags ist in
let test = if flags.strict_unit then is_unit_type else is_unit_or_eq_type in
- if test sigma (assoc_var "X1" ist) then idtac else fail
+ if test genv sigma (assoc_var "X1" ist) then idtac else fail
let bugged_is_binary sigma t =
isApp sigma t &&
@@ -121,23 +123,25 @@ let bugged_is_binary sigma t =
(** Dealing with conjunction *)
let is_conj _ ist =
+ Proofview.tclENV >>= fun genv ->
Proofview.tclEVARMAP >>= fun sigma ->
let flags = assoc_flags ist in
let ind = assoc_var "X1" ist in
if (not flags.binary_mode_bugged_detection || bugged_is_binary sigma ind) &&
- is_conjunction sigma
+ is_conjunction genv sigma
~strict:flags.strict_in_hyp_and_ccl
~onlybinary:flags.binary_mode ind
then idtac
else fail
let flatten_contravariant_conj _ ist =
+ Proofview.tclENV >>= fun genv ->
Proofview.tclEVARMAP >>= fun sigma ->
let flags = assoc_flags ist in
let typ = assoc_var "X1" ist in
let c = assoc_var "X2" ist in
let hyp = assoc_var "id" ist in
- match match_with_conjunction sigma
+ match match_with_conjunction genv sigma
~strict:flags.strict_in_contravariant_hyp
~onlybinary:flags.binary_mode typ
with
@@ -151,23 +155,25 @@ let flatten_contravariant_conj _ ist =
(** Dealing with disjunction *)
let is_disj _ ist =
+ Proofview.tclENV >>= fun genv ->
Proofview.tclEVARMAP >>= fun sigma ->
let flags = assoc_flags ist in
let t = assoc_var "X1" ist in
if (not flags.binary_mode_bugged_detection || bugged_is_binary sigma t) &&
- is_disjunction sigma
+ is_disjunction genv sigma
~strict:flags.strict_in_hyp_and_ccl
~onlybinary:flags.binary_mode t
then idtac
else fail
let flatten_contravariant_disj _ ist =
+ Proofview.tclENV >>= fun genv ->
Proofview.tclEVARMAP >>= fun sigma ->
let flags = assoc_flags ist in
let typ = assoc_var "X1" ist in
let c = assoc_var "X2" ist in
let hyp = assoc_var "id" ist in
- match match_with_disjunction sigma
+ match match_with_disjunction genv sigma
~strict:flags.strict_in_contravariant_hyp
~onlybinary:flags.binary_mode
typ with
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 350bb9019e..675e4d2457 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -194,7 +194,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
let sort = Tacticals.elimination_sort_of_goal gl in
let gl, elim =
if not is_case then
- let t,gl= pf_fresh_global (Indrec.lookup_eliminator (kn,i) sort) gl in
+ let t,gl= pf_fresh_global (Indrec.lookup_eliminator env (kn,i) sort) gl in
gl, t
else
Tacmach.pf_eapply (fun env sigma () ->
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 5abbc214de..4433f2fce7 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -340,7 +340,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
let elim, gl =
let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in
let sort = elimination_sort_of_goal gl in
- let elim, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in
+ let elim, gl = pf_fresh_global (Indrec.lookup_eliminator env ind sort) gl in
if dir = R2L then elim, gl else (* taken from Coq's rewrite *)
let elim, _ = destConst elim in
let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in
@@ -504,9 +504,9 @@ let rwprocess_rule dir rule gl =
let sigma, rs2 = loop d sigma s a.(1) rs 0 in
let s, sigma = sr sigma 1 in
loop d sigma s a.(0) rs2 0
- | App (r_eq, a) when Hipattern.match_with_equality_type sigma t != None ->
+ | App (r_eq, a) when Hipattern.match_with_equality_type env sigma t != None ->
let (ind, u) = EConstr.destInd sigma r_eq and rhs = Array.last a in
- let np = Inductiveops.inductive_nparamdecls ind in
+ let np = Inductiveops.inductive_nparamdecls env ind in
let indu = (ind, EConstr.EInstance.kind sigma u) in
let ind_ct = Inductiveops.type_of_constructors env indu in
let lhs0 = last_arg sigma (EConstr.of_constr (strip_prod_assum ind_ct.(0))) in
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 537fd7d7b4..075ebf006a 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -43,7 +43,7 @@ module AdaptorDb = struct
term_view_adaptor_db := AdaptorMap.add k (t :: lk) !term_view_adaptor_db
let subst_adaptor ( subst, (k, t as a)) =
- let t' = Detyping.subst_glob_constr subst t in
+ let t' = Detyping.subst_glob_constr (Global.env()) subst t in
if t' == t then a else k, t'
let in_db =
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 13:29:27 +0000