aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/plugin_base.dune1
-rw-r--r--plugins/ssr/ssrcommon.ml19
-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/ssrvernac.mlg2
6 files changed, 36 insertions, 18 deletions
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 1492cfb4e4..a284c3bfc7 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)
@@ -1220,7 +1217,7 @@ let genclrtac cl cs clr =
(fun type_err gl ->
tclTHEN
(tclTHEN (Proofview.V82.of_tactic (Tactics.elim_type (EConstr.of_constr
- (UnivGen.constr_of_global @@ Coqlib.(lib_ref "core.False.type"))))) (old_cleartac clr))
+ (UnivGen.constr_of_monomorphic_global @@ Coqlib.(lib_ref "core.False.type"))))) (old_cleartac clr))
(fun gl -> raise type_err)
gl))
(old_cleartac clr)
@@ -1365,7 +1362,7 @@ let tacTYPEOF c = Goal.enter_one ~__LOC__ (fun g ->
(** This tactic creates a partial proof realizing the introduction rule, but
does not check anything. *)
-let unsafe_intro env store decl b =
+let unsafe_intro env decl b =
let open Context.Named.Declaration in
Refine.refine ~typecheck:false begin fun sigma ->
let ctx = Environ.named_context_val env in
@@ -1374,7 +1371,7 @@ let unsafe_intro env store decl b =
let ninst = EConstr.mkRel 1 :: inst in
let nb = EConstr.Vars.subst1 (EConstr.mkVar (get_id decl)) b in
let sigma, ev =
- Evarutil.new_evar_instance nctx sigma nb ~principal:true ~store ninst in
+ Evarutil.new_evar_instance nctx sigma nb ~principal:true ninst in
sigma, EConstr.mkNamedLambda_or_LetIn decl ev
end
@@ -1418,7 +1415,7 @@ let-in even after reduction, it fails. In case of success, the original name
and final id are passed to the continuation [k] which gets evaluated. *)
let tclINTRO ~id ~conclusion:k = Goal.enter begin fun gl ->
let open Context in
- let env, sigma, extra, g = Goal.(env gl, sigma gl, extra gl, concl gl) in
+ let env, sigma, g = Goal.(env gl, sigma gl, concl gl) in
let decl, t, no_red = decompose_assum env sigma g in
let original_name = Rel.Declaration.get_name decl in
let already_used = Tacmach.New.pf_ids_of_hyps gl in
@@ -1433,7 +1430,7 @@ let tclINTRO ~id ~conclusion:k = Goal.enter begin fun gl ->
in
if List.mem id already_used then
errorstrm Pp.(Id.print id ++ str" already used");
- unsafe_intro env extra (set_decl_id id decl) t <*>
+ unsafe_intro env (set_decl_id id decl) t <*>
(if no_red then tclUNIT () else tclFULL_BETAIOTA) <*>
k ~orig_name:original_name ~new_name:id
end
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/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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 05:48:23 +0000