aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/funind/functional_principles_proofs.ml12
-rw-r--r--plugins/funind/invfun.ml18
-rw-r--r--plugins/funind/plugin_base.dune1
-rw-r--r--plugins/funind/recdef.ml21
-rw-r--r--plugins/ltac/plugin_base.dune1
-rw-r--r--plugins/ltac/rewrite.ml2
-rw-r--r--plugins/ltac/tacentries.ml2
-rw-r--r--plugins/ltac/tacintern.ml4
-rw-r--r--plugins/ltac/tacintern.mli4
-rw-r--r--plugins/ltac/tacinterp.ml4
-rw-r--r--plugins/ssr/plugin_base.dune1
-rw-r--r--plugins/ssr/ssrcommon.ml11
-rw-r--r--plugins/ssr/ssrcommon.mli3
-rw-r--r--plugins/ssr/ssreflect.v18
-rw-r--r--plugins/ssr/ssrelim.ml11
-rw-r--r--plugins/ssr/ssrequality.ml6
-rw-r--r--plugins/ssrmatching/plugin_base.dune1
-rw-r--r--plugins/ssrmatching/ssrmatching.ml2
18 files changed, 58 insertions, 64 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index ad1114b733..d4e410bd69 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -229,10 +229,6 @@ let isAppConstruct ?(env=Global.env ()) sigma t =
true
with Not_found -> false
-let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *)
- Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env @@ Evd.from_env Environ.empty_env
-
-
exception NoChange
let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
@@ -420,7 +416,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
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
- let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in
+ let reduced_type_of_hyp = Reductionops.nf_betaiotazeta env sigma real_type_of_hyp in
(* length of context didn't change ? *)
let new_context,new_typ_of_hyp =
decompose_prod_n_assum sigma (List.length context) reduced_type_of_hyp
@@ -800,7 +796,7 @@ let build_proof
g
| LetIn _ ->
let new_infos =
- { dyn_infos with info = nf_betaiotazeta dyn_infos.info }
+ { dyn_infos with info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info }
in
tclTHENLIST
@@ -834,7 +830,7 @@ let build_proof
| LetIn _ ->
let new_infos =
{ dyn_infos with
- info = nf_betaiotazeta dyn_infos.info
+ info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info
}
in
@@ -977,7 +973,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
(* observe (str "body " ++ pr_lconstr bodies.(num)); *)
let f_body_with_params_and_other_fun = substl fnames_with_params bodies.(num) in
(* observe (str "f_body_with_params_and_other_fun " ++ pr_lconstr f_body_with_params_and_other_fun); *)
- let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
+ let eq_rhs = Reductionops.nf_betaiotazeta (Global.env ()) evd (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
(* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *)
let (type_ctxt,type_of_f),evd =
let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd f
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b0842c3721..96eb7fbc60 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -63,12 +63,6 @@ let observe_tac s tac g =
then do_observe_tac (str s) tac g
else tac g
-(* [nf_zeta] $\zeta$-normalization of a term *)
-let nf_zeta =
- Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
- Environ.empty_env
- (Evd.from_env Environ.empty_env)
-
let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
(* (\* [id_to_constr id] finds the term associated to [id] in the global environment *\) *)
@@ -219,7 +213,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
let mib,_ = Global.lookup_inductive graph_ind in
(* and the principle to use in this lemma in $\zeta$ normal form *)
let f_principle,princ_type = schemes.(i) in
- let princ_type = nf_zeta princ_type in
+ let princ_type = Reductionops.nf_zeta (Global.env ()) evd princ_type in
let princ_infos = Tactics.compute_elim_sig evd princ_type in
(* The number of args of the function is then easily computable *)
let nb_fun_args = nb_prod (project g) (pf_concl g) - 2 in
@@ -397,7 +391,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
List.rev (fst (List.fold_left2
(fun (bindings,avoid) decl p ->
let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in
- (nf_zeta p)::bindings,id::avoid)
+ (Reductionops.nf_zeta (pf_env g) (project g) p)::bindings,id::avoid)
([],avoid)
princ_infos.predicates
(lemmas)))
@@ -630,12 +624,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti
*)
let lemmas =
Array.map
- (fun (_,(ctxt,concl)) -> nf_zeta (EConstr.it_mkLambda_or_LetIn concl ctxt))
+ (fun (_,(ctxt,concl)) -> Reductionops.nf_zeta (pf_env g) (project g) (EConstr.it_mkLambda_or_LetIn concl ctxt))
lemmas_types_infos
in
(* We get the constant and the principle corresponding to this lemma *)
let f = funcs.(i) in
- let graph_principle = nf_zeta (EConstr.of_constr schemes.(i)) in
+ let graph_principle = Reductionops.nf_zeta (pf_env g) (project g) (EConstr.of_constr schemes.(i)) in
let princ_type = pf_unsafe_type_of g graph_principle in
let princ_infos = Tactics.compute_elim_sig (project g) princ_type in
(* Then we get the number of argument of the function
@@ -771,7 +765,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
let sigma, _ = Typing.type_of (Global.env ()) !evd type_of_lemma in
evd := sigma;
- let type_of_lemma = nf_zeta type_of_lemma in
+ let type_of_lemma = Reductionops.nf_zeta (Global.env ()) !evd type_of_lemma in
observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma);
type_of_lemma,type_info
)
@@ -838,7 +832,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
let type_of_lemma =
EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
in
- let type_of_lemma = nf_zeta type_of_lemma in
+ let type_of_lemma = Reductionops.nf_zeta env !evd type_of_lemma in
observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env env !evd type_of_lemma);
type_of_lemma,type_info
)
diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/plugin_base.dune
index 002eb28eea..9f583234d8 100644
--- a/plugins/funind/plugin_base.dune
+++ b/plugins/funind/plugin_base.dune
@@ -2,4 +2,5 @@
(name recdef_plugin)
(public_name coq.plugins.recdef)
(synopsis "Coq's functional induction plugin")
+ (flags :standard -open Gramlib)
(libraries coq.plugins.extraction))
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index f9df3aed45..63a3e0582d 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -103,21 +103,6 @@ let const_of_ref = function
ConstRef kn -> kn
| _ -> anomaly (Pp.str "ConstRef expected.")
-
-let nf_zeta env =
- Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
- env (Evd.from_env env)
-
-
-let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *)
- Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env
- (Evd.from_env Environ.empty_env)
-
-
-
-
-
-
(* Generic values *)
let pf_get_new_ids idl g =
let ids = pf_ids_of_hyps g in
@@ -747,7 +732,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
with
| UserError(Some "Refiner.thensn_tac3",_)
| UserError(Some "Refiner.tclFAIL_s",_) ->
- (observe_tac (str "is computable " ++ Printer.pr_leconstr_env (pf_env g) sigma new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} )
+ (observe_tac (str "is computable " ++ Printer.pr_leconstr_env (pf_env g) sigma new_info.info) (next_step continuation_tac {new_info with info = Reductionops.nf_betaiotazeta (pf_env g) sigma new_info.info} )
))
g
@@ -1537,13 +1522,13 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
(* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *)
let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in
let evd = Evd.minimize_universes evd in
- let equation_lemma_type = nf_betaiotazeta (Evarutil.nf_evar evd ty) in
+ let equation_lemma_type = Reductionops.nf_betaiotazeta env evd (Evarutil.nf_evar evd ty) in
let function_type = EConstr.to_constr ~abort_on_undefined_evars:false evd function_type in
let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in
(* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *)
let res_vars,eq' = decompose_prod equation_lemma_type in
let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> LocalAssum (x,y)) res_vars) env in
- let eq' = nf_zeta env_eq' (EConstr.of_constr eq') in
+ let eq' = Reductionops.nf_zeta env_eq' evd (EConstr.of_constr eq') in
let eq' = EConstr.Unsafe.to_constr eq' in
let res =
(* Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *)
diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/plugin_base.dune
index 5611f5ba16..1b31655310 100644
--- a/plugins/ltac/plugin_base.dune
+++ b/plugins/ltac/plugin_base.dune
@@ -3,6 +3,7 @@
(public_name coq.plugins.ltac)
(synopsis "Coq's LTAC tactic language")
(modules :standard \ tauto)
+ (flags :standard -open Gramlib)
(libraries coq.stm))
(library
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 9f7669f1d5..8b2721ae4e 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1492,7 +1492,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
if not (Evd.is_defined acc ev) then
user_err ~hdr:"rewrite"
(str "Unsolved constraint remaining: " ++ spc () ++
- Termops.pr_evar_info (Evd.find acc ev))
+ Termops.pr_evar_info env acc (Evd.find acc ev))
else Evd.remove acc ev)
cstrs evars'
in
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 16cff420bd..0f88734caf 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -353,7 +353,7 @@ let extend_atomic_tactic name entries =
let default = epsilon_value inj e in
match default with
| None -> raise NonEmptyArgument
- | Some def -> Tacintern.intern_tactic_or_tacarg Tacintern.fully_empty_glob_sign def
+ | Some def -> Tacintern.intern_tactic_or_tacarg (Genintern.empty_glob_sign Environ.empty_env) def
in
try Some (hd, List.map empty_value rem) with NonEmptyArgument -> None
in
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 55412c74bb..fcbcfae115 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -46,7 +46,6 @@ type glob_sign = Genintern.glob_sign = {
extra : Genintern.Store.t;
}
-let fully_empty_glob_sign = Genintern.empty_glob_sign Environ.empty_env
let make_empty_glob_sign () = Genintern.empty_glob_sign (Global.env ())
(* We have identifier <| global_reference <| constr *)
@@ -83,7 +82,8 @@ let intern_hyp ist ({loc;v=id} as locid) =
else if find_ident id ist then
make id
else
- Pretype_errors.error_var_not_found ?loc id
+ CErrors.user_err ?loc Pp.(str "Hypothesis" ++ spc () ++ Id.print id ++ spc() ++
+ str "was not found in the current environment.")
let intern_or_var f ist = function
| ArgVar locid -> ArgVar (intern_hyp ist locid)
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index 9146fced2d..a9f2d76e30 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -23,10 +23,8 @@ type glob_sign = Genintern.glob_sign = {
extra : Genintern.Store.t;
}
-val fully_empty_glob_sign : glob_sign
-
val make_empty_glob_sign : unit -> glob_sign
- (** same as [fully_empty_glob_sign], but with [Global.env()] as
+ (** build an empty [glob_sign] using [Global.env()] as
environment *)
(** Main globalization functions *)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index b60b77595b..5828494454 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -686,7 +686,7 @@ let interp_may_eval f ist env sigma = function
| ConstrContext ({loc;v=s},c) ->
(try
let (sigma,ic) = f ist env sigma c in
- let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in
+ let ctxt = try_interp_ltac_var coerce_to_constr_context ist (Some (env, sigma)) (make ?loc s) in
let ctxt = EConstr.Unsafe.to_constr ctxt in
let ic = EConstr.Unsafe.to_constr ic in
let c = subst_meta [Constr_matching.special_meta,ic] ctxt in
@@ -2024,7 +2024,7 @@ let interp_ltac_constr ist c k = Ftactic.run (interp_ltac_constr ist c) k
let interp_redexp env sigma r =
let ist = default_ist () in
- let gist = { fully_empty_glob_sign with genv = env; } in
+ let gist = Genintern.empty_glob_sign env in
interp_red_expr ist env sigma (intern_red_expr gist r)
(***************************************************************************)
diff --git a/plugins/ssr/plugin_base.dune b/plugins/ssr/plugin_base.dune
index de9053f1a0..a13524bb52 100644
--- a/plugins/ssr/plugin_base.dune
+++ b/plugins/ssr/plugin_base.dune
@@ -3,4 +3,5 @@
(public_name coq.plugins.ssreflect)
(synopsis "Coq's ssreflect plugin")
(modules_without_implementation ssrast)
+ (flags :standard -open Gramlib)
(libraries coq.plugins.ssrmatching))
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 70a2a30cd5..5d75b28539 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -730,13 +730,10 @@ let pf_abs_prod name gl c cl = pf_mkprod gl c ~name (Termops.subst_term (project
(** look up a name in the ssreflect internals module *)
let ssrdirpath = DirPath.make [Id.of_string "ssreflect"]
let ssrqid name = Libnames.make_qualid ssrdirpath (Id.of_string name)
-let ssrtopqid name = Libnames.qualid_of_ident (Id.of_string name)
-let locate_reference qid =
- Smartlocate.global_of_extended_global (Nametab.locate_extended qid)
let mkSsrRef name =
- try locate_reference (ssrqid name) with Not_found ->
- try locate_reference (ssrtopqid name) with Not_found ->
- CErrors.user_err (Pp.str "Small scale reflection library not loaded")
+ let qn = Format.sprintf "plugins.ssreflect.%s" name in
+ if Coqlib.has_ref qn then Coqlib.lib_ref qn else
+ CErrors.user_err Pp.(str "Small scale reflection library not loaded (" ++ str name ++ str ")")
let mkSsrRRef name = (DAst.make @@ GRef (mkSsrRef name,None)), None
let mkSsrConst name env sigma =
EConstr.fresh_global env sigma (mkSsrRef name)
@@ -943,7 +940,7 @@ let pf_saturate ?beta ?bi_types gl c ?ty m =
let pf_partial_solution gl t evl =
let sigma, g = project gl, sig_it gl in
- let sigma = Goal.V82.partial_solution sigma g t in
+ let sigma = Goal.V82.partial_solution (pf_env gl) sigma g t in
re_sig (List.map (fun x -> (fst (EConstr.destEvar sigma x))) evl) sigma
let dependent_apply_error =
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 9ba23467e7..566a933522 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -212,8 +212,7 @@ val pf_abs_prod :
EConstr.t -> Goal.goal Evd.sigma * EConstr.types
val mkSsrRRef : string -> Glob_term.glob_constr * 'a option
-val mkSsrRef : string -> GlobRef.t
-val mkSsrConst :
+val mkSsrConst :
string ->
env -> evar_map -> evar_map * EConstr.t
val pf_mkSsrConst :
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index 460bdc6d23..e43cab094b 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -159,6 +159,10 @@ Definition abstract (statement : Type) (id : nat) (lock : abstract_lock) :=
Notation "<hidden n >" := (abstract _ n _).
Notation "T (* n *)" := (abstract T n abstract_key).
+Register abstract_lock as plugins.ssreflect.abstract_lock.
+Register abstract_key as plugins.ssreflect.abstract_key.
+Register abstract as plugins.ssreflect.abstract.
+
(* Constants for tactic-views *)
Inductive external_view : Type := tactic_view of Type.
@@ -287,6 +291,8 @@ Variant phant (p : Type) := Phant.
Definition protect_term (A : Type) (x : A) : A := x.
+Register protect_term as plugins.ssreflect.protect_term.
+
(* The ssreflect idiom for a non-keyed pattern: *)
(* - unkeyed t wiil match any subterm that unifies with t, regardless of *)
(* whether it displays the same head symbol as t. *)
@@ -336,6 +342,9 @@ Notation nosimpl t := (let: tt := tt in t).
Lemma master_key : unit. Proof. exact tt. Qed.
Definition locked A := let: tt := master_key in fun x : A => x.
+Register master_key as plugins.ssreflect.master_key.
+Register locked as plugins.ssreflect.locked.
+
Lemma lock A x : x = locked x :> A. Proof. unlock; reflexivity. Qed.
(* Needed for locked predicates, in particular for eqType's. *)
@@ -395,12 +404,18 @@ Definition ssr_have_let Pgoal Plemma step
(rest : let x : Plemma := step in Pgoal) : Pgoal := rest.
Arguments ssr_have_let [Pgoal].
+Register ssr_have as plugins.ssreflect.ssr_have.
+Register ssr_have_let as plugins.ssreflect.ssr_have_let.
+
Definition ssr_suff Plemma Pgoal step (rest : Plemma) : Pgoal := step rest.
Arguments ssr_suff Plemma [Pgoal].
Definition ssr_wlog := ssr_suff.
Arguments ssr_wlog Plemma [Pgoal].
+Register ssr_suff as plugins.ssreflect.ssr_suff.
+Register ssr_wlog as plugins.ssreflect.ssr_wlog.
+
(* Internal N-ary congruence lemmas for the congr tactic. *)
Fixpoint nary_congruence_statement (n : nat)
@@ -425,6 +440,9 @@ Lemma ssr_congr_arrow Plemma Pgoal : Plemma = Pgoal -> Plemma -> Pgoal.
Proof. by move->. Qed.
Arguments ssr_congr_arrow : clear implicits.
+Register nary_congruence as plugins.ssreflect.nary_congruence.
+Register ssr_congr_arrow as plugins.ssreflect.ssr_congr_arrow.
+
(* View lemmas that don't use reflection. *)
Section ApplyIff.
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 7f9a9e125e..5067d8af31 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -16,7 +16,6 @@ open Printer
open Term
open Constr
open Termops
-open Globnames
open Tactypes
open Tacmach
@@ -98,6 +97,11 @@ let subgoals_tys sigma (relctx, concl) =
* generalize the equality in case eqid is not None
* 4. build the tactic handle intructions and clears as required in ipats and
* by eqid *)
+
+let get_eq_type gl =
+ let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in
+ gl, EConstr.of_constr eq
+
let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac gl =
(* some sanity checks *)
let oc, orig_clr, occ, c_gen, gl = match what with
@@ -115,8 +119,6 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac
let orig_gl, concl, env = gl, pf_concl gl, pf_env gl in
ppdebug(lazy(Pp.str(if is_case then "==CASE==" else "==ELIM==")));
let fire_subst gl t = Reductionops.nf_evar (project gl) t in
- let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in
- let eq = EConstr.of_constr eq in
let is_undef_pat = function
| sigma, T t -> EConstr.isEvar sigma (EConstr.of_constr t)
| _ -> false in
@@ -322,6 +324,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac
let k = List.length deps in
let c = fire_subst gl (List.assoc (n_elim_args - k - 1) elim_args) in
let gl, t = pfe_type_of gl c in
+ let gl, eq = get_eq_type gl in
let gen_eq_tac, gl =
let refl = EConstr.mkApp (eq, [|t; c; c|]) in
let new_concl = EConstr.mkArrow refl (EConstr.Vars.lift 1 (pf_concl orig_gl)) in
@@ -421,7 +424,7 @@ let injectl2rtac sigma c = match EConstr.kind sigma c with
let is_injection_case c gl =
let gl, cty = pfe_type_of gl c in
let (mind,_), _ = pf_reduce_to_quantified_ind gl cty in
- GlobRef.equal (IndRef mind) Coqlib.(lib_ref "core.eq.type")
+ Coqlib.check_ind_ref "core.eq.type" mind
let perform_injection c gl =
let gl, cty = pfe_type_of gl c in
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index c04ced4ab4..036b20bfcd 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -433,15 +433,15 @@ let lz_coq_prod =
let lz_setoid_relation =
let sdir = ["Classes"; "RelationClasses"] in
- let last_srel = ref (Environ.empty_env, None) in
+ let last_srel = ref None in
fun env -> match !last_srel with
- | env', srel when env' == env -> srel
+ | Some (env', srel) when env' == env -> srel
| _ ->
let srel =
try Some (UnivGen.constr_of_global @@
Coqlib.find_reference "Class_setoid" ("Coq"::sdir) "RewriteRelation" [@ocaml.warning "-3"])
with _ -> None in
- last_srel := (env, srel); srel
+ last_srel := Some (env, srel); srel
let ssr_is_setoid env =
match lz_setoid_relation env with
diff --git a/plugins/ssrmatching/plugin_base.dune b/plugins/ssrmatching/plugin_base.dune
index 06f67c3774..1450a94de1 100644
--- a/plugins/ssrmatching/plugin_base.dune
+++ b/plugins/ssrmatching/plugin_base.dune
@@ -2,4 +2,5 @@
(name ssrmatching_plugin)
(public_name coq.plugins.ssrmatching)
(synopsis "Coq ssrmatching plugin")
+ (flags :standard -open Gramlib)
(libraries coq.plugins.ltac))
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 7f67487f5d..bb6decd848 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -1048,7 +1048,7 @@ let thin id sigma goal =
| None -> sigma
| Some (sigma, hyps, concl) ->
let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl in
- let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
+ let sigma = Goal.V82.partial_solution_to env sigma goal gl ev in
sigma
(*
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 15:18:36 +0000