aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrbool.v16
-rw-r--r--plugins/ssr/ssrcommon.ml2
-rw-r--r--plugins/ssr/ssreflect.v6
-rw-r--r--plugins/ssr/ssrfun.v4
-rw-r--r--plugins/ssr/ssrfwd.ml10
-rw-r--r--plugins/ssr/ssripats.ml5
-rw-r--r--plugins/ssr/ssrparser.ml43
-rw-r--r--plugins/ssr/ssrparser.mli4
-rw-r--r--plugins/ssr/ssrvernac.ml414
9 files changed, 29 insertions, 35 deletions
diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index 7d05b64384..0865f75ec5 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -61,8 +61,8 @@ Require Import ssreflect ssrfun.
(* classically P <-> we can assume P when proving is_true b. *)
(* := forall b : bool, (P -> b) -> b. *)
(* This is equivalent to ~ (~ P) when P : Prop. *)
-(* implies P Q == wrapper coinductive type that coerces to P -> Q *)
-(* and can be used as a P -> Q view unambigously. *)
+(* implies P Q == wrapper variant type that coerces to P -> Q and *)
+(* can be used as a P -> Q view unambigously. *)
(* Useful to avoid spurious insertion of <-> views *)
(* when Q is a conjunction of foralls, as in Lemma *)
(* all_and2 below; conversely, avoids confusion in *)
@@ -456,7 +456,7 @@ Section BoolIf.
Variables (A B : Type) (x : A) (f : A -> B) (b : bool) (vT vF : A).
-CoInductive if_spec (not_b : Prop) : bool -> A -> Set :=
+Variant if_spec (not_b : Prop) : bool -> A -> Set :=
| IfSpecTrue of b : if_spec not_b true vT
| IfSpecFalse of not_b : if_spec not_b false vF.
@@ -585,7 +585,7 @@ Lemma rwP2 : reflect Q b -> (P <-> Q).
Proof. by move=> Qb; split=> ?; [apply: appP | apply: elimT; case: Qb]. Qed.
(* Predicate family to reflect excluded middle in bool. *)
-CoInductive alt_spec : bool -> Type :=
+Variant alt_spec : bool -> Type :=
| AltTrue of P : alt_spec true
| AltFalse of ~~ b : alt_spec false.
@@ -603,7 +603,7 @@ Hint View for apply// equivPif|3 xorPif|3 equivPifn|3 xorPifn|3.
(* Allow the direct application of a reflection lemma to a boolean assertion. *)
Coercion elimT : reflect >-> Funclass.
-CoInductive implies P Q := Implies of P -> Q.
+Variant implies P Q := Implies of P -> Q.
Lemma impliesP P Q : implies P Q -> P -> Q. Proof. by case. Qed.
Lemma impliesPn (P Q : Prop) : implies P Q -> ~ Q -> ~ P.
Proof. by case=> iP ? /iP. Qed.
@@ -1119,7 +1119,7 @@ Proof. by move=> *; apply/orP; left. Qed.
Lemma subrelUr r1 r2 : subrel r2 (relU r1 r2).
Proof. by move=> *; apply/orP; right. Qed.
-CoInductive mem_pred := Mem of pred T.
+Variant mem_pred := Mem of pred T.
Definition isMem pT topred mem := mem = (fun p : pT => Mem [eta topred p]).
@@ -1329,7 +1329,7 @@ End simpl_mem.
(* Qualifiers and keyed predicates. *)
-CoInductive qualifier (q : nat) T := Qualifier of predPredType T.
+Variant qualifier (q : nat) T := Qualifier of predPredType T.
Coercion has_quality n T (q : qualifier n T) : pred_class :=
fun x => let: Qualifier _ p := q in p x.
@@ -1376,7 +1376,7 @@ Notation "[ 'qualify' 'an' x : T | P ]" := (Qualifier 2 (fun x : T => P%B))
Section KeyPred.
Variable T : Type.
-CoInductive pred_key (p : predPredType T) := DefaultPredKey.
+Variant pred_key (p : predPredType T) := DefaultPredKey.
Variable p : predPredType T.
Structure keyed_pred (k : pred_key p) :=
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 54f3f9c718..1f3c758e5c 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -469,7 +469,7 @@ let ssrevaltac ist gtac = Tacinterp.tactic_of_value ist gtac
(* term mkApp (t', args) is convertible to t. *)
(* This makes a useful shorthand for local definitions in proofs, *)
(* i.e., pose succ := _ + 1 means pose succ := fun n : nat => n + 1, *)
-(* and, in context of the the 4CT library, pose mid := maps id means *)
+(* and, in context of the 4CT library, pose mid := maps id means *)
(* pose mid := fun d : detaSet => @maps d d (@id (datum d)) *)
(* Note that this facility does not extend to set, which tries *)
(* instead to fill holes by matching a goal subterm. *)
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index b0a9441385..b4144aa45e 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -184,7 +184,7 @@ Inductive external_view : Type := tactic_view of Type.
Module TheCanonical.
-CoInductive put vT sT (v1 v2 : vT) (s : sT) := Put.
+Variant put vT sT (v1 v2 : vT) (s : sT) := Put.
Definition get vT sT v s (p : @put vT sT v v s) := let: Put _ _ _ := p in s.
@@ -275,10 +275,10 @@ Notation "{ 'type' 'of' c 'for' s }" := (dependentReturnType c s)
(* We also define a simpler version ("phant" / "Phant") of phantom for the *)
(* common case where p_type is Type. *)
-CoInductive phantom T (p : T) := Phantom.
+Variant phantom T (p : T) := Phantom.
Arguments phantom : clear implicits.
Arguments Phantom : clear implicits.
-CoInductive phant (p : Type) := Phant.
+Variant phant (p : Type) := Phant.
(* Internal tagging used by the implementation of the ssreflect elim. *)
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index ac2c78249b..b2d5143e36 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -326,7 +326,7 @@ Section SimplFun.
Variables aT rT : Type.
-CoInductive simpl_fun := SimplFun of aT -> rT.
+Variant simpl_fun := SimplFun of aT -> rT.
Definition fun_of_simpl f := fun x => let: SimplFun lam := f in lam x.
@@ -684,7 +684,7 @@ Section Bijections.
Variables (A B : Type) (f : B -> A).
-CoInductive bijective : Prop := Bijective g of cancel f g & cancel g f.
+Variant bijective : Prop := Bijective g of cancel f g & cancel g f.
Hypothesis bijf : bijective.
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 7fe2421f90..e367cd32d6 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -68,20 +68,14 @@ open Ssripats
let ssrhaveNOtcresolution = Summary.ref ~name:"SSR:havenotcresolution" false
-let inHaveTCResolution = Libobject.declare_object {
- (Libobject.default_object "SSRHAVETCRESOLUTION") with
- Libobject.cache_function = (fun (_,v) -> ssrhaveNOtcresolution := v);
- Libobject.load_function = (fun _ (_,v) -> ssrhaveNOtcresolution := v);
- Libobject.classify_function = (fun v -> Libobject.Keep v);
-}
let _ =
Goptions.declare_bool_option
{ Goptions.optname = "have type classes";
Goptions.optkey = ["SsrHave";"NoTCResolution"];
Goptions.optread = (fun _ -> !ssrhaveNOtcresolution);
Goptions.optdepr = false;
- Goptions.optwrite = (fun b ->
- Lib.add_anonymous_leaf (inHaveTCResolution b)) }
+ Goptions.optwrite = (fun b -> ssrhaveNOtcresolution := b);
+ }
open Constrexpr
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 46fde41150..1dbacf0ff7 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -379,8 +379,9 @@ let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr =
let ctx, last = EConstr.decompose_prod_assum sigma concl in
let args = match EConstr.kind_of_type sigma last with
| Term.AtomicType (hd, args) ->
- assert(Ssrcommon.is_protect hd env sigma);
- args
+ if Ssrcommon.is_protect hd env sigma then args
+ else Ssrcommon.errorstrm
+ (Pp.str "Too many names in intro pattern")
| _ -> assert false in
let case = args.(Array.length args-1) in
if not(EConstr.Vars.closed0 sigma case)
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 347a1e4e26..8b9c94f2db 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -962,6 +962,7 @@ END
(* the default simpl and unfold tactics would erase blindly. *)
open Ssrmatching_plugin.Ssrmatching
+open Ssrmatching_plugin.G_ssrmatching
let pr_wgen = function
| (clr, Some((id,k),None)) -> spc() ++ pr_clear mt clr ++ str k ++ pr_hoi id
@@ -1407,7 +1408,7 @@ let check_seqtacarg dir arg = match snd arg, dir with
CErrors.user_err ?loc (str "expected \"first\"")
| _, _ -> arg
-let ssrorelse = Gram.entry_create "ssrorelse"
+let ssrorelse = Entry.create "ssrorelse"
GEXTEND Gram
GLOBAL: ssrorelse ssrseqarg;
ssrseqidx: [
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index 7cd3751cef..862a93765d 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -12,11 +12,11 @@
open Ltac_plugin
-val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
+val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t
val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
val pr_ssrtacarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c) -> 'c
-val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
+val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t
val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
val pr_ssrtclarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 7ce2dd64af..989a6c5bf1 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -24,7 +24,6 @@ open Ltac_plugin
open Notation_ops
open Notation_term
open Glob_term
-open Globnames
open Stdarg
open Genarg
open Decl_kinds
@@ -218,8 +217,8 @@ let interp_search_notation ?loc tag okey =
(Bytes.set s' i' '_'; loop (j + 1) (i' + 2))
else (String.blit s i s' i' m; loop (j + 1) (i' + m + 1)) in
loop 0 1 in
- let trim_ntn (pntn, m) = Bytes.sub_string pntn 1 (max 0 m) in
- let pr_ntn ntn = str "(" ++ str ntn ++ str ")" in
+ let trim_ntn (pntn, m) = (InConstrEntrySomeLevel,Bytes.sub_string pntn 1 (max 0 m)) in
+ let pr_ntn ntn = str "(" ++ Notation.pr_notation ntn ++ str ")" in
let pr_and_list pr = function
| [x] -> pr x
| x :: lx -> pr_list pr_comma pr lx ++ pr_comma () ++ str "and " ++ pr x
@@ -294,7 +293,7 @@ let interp_search_notation ?loc tag okey =
let scs' = List.remove (=) sc !scs in
let w = pr_ntn ntn ++ str " is also defined " ++ pr_scs scs' in
Feedback.msg_warning (hov 4 w)
- else if String.string_contains ~where:ntn ~what:" .. " then
+ else if String.string_contains ~where:(snd ntn) ~what:" .. " then
err (pr_ntn ntn ++ str " is an n-ary notation");
let nvars = List.filter (fun (_,(_,typ)) -> typ = NtnTypeConstr) nvars in
let rec sub () = function
@@ -359,13 +358,12 @@ let coerce_search_pattern_to_sort hpat =
true, cp
with _ -> false, [] in
let coerce hp coe_index =
- let coe = Classops.get_coercion_value coe_index in
+ let coe_ref = coe_index.Classops.coe_value in
try
- let coe_ref = global_of_constr coe in
let n_imps = Option.get (Classops.hide_coercion coe_ref) in
mkPApp (Pattern.PRef coe_ref) n_imps [|hp|]
- with _ ->
- errorstrm (str "need explicit coercion " ++ pr_constr_env env sigma coe ++ spc ()
+ with Not_found | Option.IsNone ->
+ errorstrm (str "need explicit coercion " ++ pr_global coe_ref ++ spc ()
++ str "to interpret head search pattern as type") in
filter_head, List.fold_left coerce hpat' coe_path
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 05:18:02 +0000