aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrbool.v8
-rw-r--r--plugins/ssr/ssrcommon.ml5
-rw-r--r--plugins/ssr/ssrcommon.mli1
-rw-r--r--plugins/ssr/ssreflect.v1
-rw-r--r--plugins/ssr/ssrequality.ml48
-rw-r--r--plugins/ssr/ssrfun.v10
-rw-r--r--plugins/ssr/ssrparser.mlg64
-rw-r--r--plugins/ssr/ssrvernac.mlg9
8 files changed, 69 insertions, 77 deletions
diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index bf0761d3ae..376410658a 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -1323,7 +1323,6 @@ Proof. by move=> x y r2xy; apply/orP; right. Qed.
(** Variant of simpl_pred specialised to the membership operator. **)
-#[universes(template)]
Variant mem_pred T := Mem of pred T.
(**
@@ -1464,7 +1463,6 @@ Implicit Types (mp : mem_pred T).
Definition Acoll : collective_pred T := [pred x | ...].
as the collective_pred_of_simpl is _not_ convertible to pred_of_simpl. **)
-#[universes(template)]
Structure registered_applicative_pred p := RegisteredApplicativePred {
applicative_pred_value :> pred T;
_ : applicative_pred_value = p
@@ -1473,21 +1471,18 @@ Definition ApplicativePred p := RegisteredApplicativePred (erefl p).
Canonical applicative_pred_applicative sp :=
ApplicativePred (applicative_pred_of_simpl sp).
-#[universes(template)]
Structure manifest_simpl_pred p := ManifestSimplPred {
simpl_pred_value :> simpl_pred T;
_ : simpl_pred_value = SimplPred p
}.
Canonical expose_simpl_pred p := ManifestSimplPred (erefl (SimplPred p)).
-#[universes(template)]
Structure manifest_mem_pred p := ManifestMemPred {
mem_pred_value :> mem_pred T;
_ : mem_pred_value = Mem [eta p]
}.
Canonical expose_mem_pred p := ManifestMemPred (erefl (Mem [eta p])).
-#[universes(template)]
Structure applicative_mem_pred p :=
ApplicativeMemPred {applicative_mem_pred_value :> manifest_mem_pred p}.
Canonical check_applicative_mem_pred p (ap : registered_applicative_pred p) :=
@@ -1538,7 +1533,6 @@ End PredicateSimplification.
(** Qualifiers and keyed predicates. **)
-#[universes(template)]
Variant qualifier (q : nat) T := Qualifier of {pred T}.
Coercion has_quality n T (q : qualifier n T) : {pred T} :=
@@ -1573,7 +1567,6 @@ Variable T : Type.
Variant pred_key (p : {pred T}) := DefaultPredKey.
Variable p : {pred T}.
-#[universes(template)]
Structure keyed_pred (k : pred_key p) :=
PackKeyedPred {unkey_pred :> {pred T}; _ : unkey_pred =i p}.
@@ -1605,7 +1598,6 @@ Section KeyedQualifier.
Variables (T : Type) (n : nat) (q : qualifier n T).
-#[universes(template)]
Structure keyed_qualifier (k : pred_key q) :=
PackKeyedQualifier {unkey_qualifier; _ : unkey_qualifier = q}.
Definition KeyedQualifier k := PackKeyedQualifier k (erefl q).
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 33e9f871fd..dbb60e6712 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -181,7 +181,6 @@ let option_assert_get o msg =
(** Constructors for rawconstr *)
open Glob_term
-open Decl_kinds
let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None)
@@ -681,6 +680,10 @@ let pf_type_id gl t = Id.of_string (Namegen.hdchar (pf_env gl) (project gl) t)
let pfe_type_of gl t =
let sigma, ty = pf_type_of gl t in
re_sig (sig_it gl) sigma, ty
+let pfe_new_type gl =
+ let sigma, env, it = project gl, pf_env gl, sig_it gl in
+ let sigma,t = Evarutil.new_Type sigma in
+ re_sig it sigma, t
let pfe_type_relevance_of gl t =
let gl, ty = pfe_type_of gl t in
gl, ty, pf_apply Retyping.relevance_of_term gl t
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index e920bc318a..db1d2d456e 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -205,6 +205,7 @@ val pf_type_of :
val pfe_type_of :
Goal.goal Evd.sigma ->
EConstr.t -> Goal.goal Evd.sigma * EConstr.types
+val pfe_new_type : Goal.goal Evd.sigma -> Goal.goal Evd.sigma * EConstr.types
val pfe_type_relevance_of :
Goal.goal Evd.sigma ->
EConstr.t -> Goal.goal Evd.sigma * EConstr.types * Sorts.relevance
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index 71abafc22f..9ebdf71329 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -209,7 +209,6 @@ Register abstract_key as plugins.ssreflect.abstract_key.
Register abstract as plugins.ssreflect.abstract.
(** Constants for tactic-views **)
-#[universes(template)]
Inductive external_view : Type := tactic_view of Type.
(**
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index aa1316f15e..742890637a 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -109,6 +109,11 @@ let congrtac ((n, t), ty) ist gl =
loop 1 in
tclTHEN (refine_with cf) (tclTRY (Proofview.V82.of_tactic Tactics.reflexivity)) gl
+let pf_typecheck t gl =
+ let it = sig_it gl in
+ let sigma,_ = pf_type_of gl t in
+ re_sig [it] sigma
+
let newssrcongrtac arg ist gl =
ppdebug(lazy Pp.(str"===newcongr==="));
ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl)));
@@ -128,17 +133,23 @@ let newssrcongrtac arg ist gl =
x, re_sig si sigma in
let arr, gl = pf_mkSsrConst "ssr_congr_arrow" gl in
let ssr_congr lr = EConstr.mkApp (arr, lr) in
+ let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in
(* here the two cases: simple equality or arrow *)
- let equality, _, eq_args, gl' =
- let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in
- pf_saturate gl (EConstr.of_constr eq) 3 in
+ let equality, _, eq_args, gl' = pf_saturate gl (EConstr.of_constr eq) 3 in
tclMATCH_GOAL (equality, gl') (fun gl' -> fs gl' (List.assoc 0 eq_args))
(fun ty -> congrtac (arg, Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) ty) ist)
(fun () ->
- let lhs, gl' = mk_evar gl EConstr.mkProp in let rhs, gl' = mk_evar gl' EConstr.mkProp in
+ let gl', t_lhs = pfe_new_type gl in
+ let gl', t_rhs = pfe_new_type gl' in
+ let lhs, gl' = mk_evar gl' t_lhs in
+ let rhs, gl' = mk_evar gl' t_rhs in
let arrow = EConstr.mkArrow lhs Sorts.Relevant (EConstr.Vars.lift 1 rhs) in
tclMATCH_GOAL (arrow, gl') (fun gl' -> [|fs gl' lhs;fs gl' rhs|])
- (fun lr -> tclTHEN (Proofview.V82.of_tactic (Tactics.apply (ssr_congr lr))) (congrtac (arg, mkRType) ist))
+ (fun lr ->
+ let a = ssr_congr lr in
+ tclTHENLIST [ pf_typecheck a
+ ; Proofview.V82.of_tactic (Tactics.apply a)
+ ; congrtac (arg, mkRType) ist ])
(fun _ _ -> errorstrm Pp.(str"Conclusion is not an equality nor an arrow")))
gl
@@ -336,17 +347,21 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_
let sigma, p = (* The resulting goal *)
Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in
let pred = EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdx_ty pred in
- let elim, gl =
- let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in
+ let sigma, elim =
let sort = elimination_sort_of_goal 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
- let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in
- let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in
- mkConst c1', gl in
- let elim = EConstr.of_constr elim in
+ match Equality.eq_elimination_ref (dir = L2R) sort with
+ | Some r -> Evd.fresh_global env sigma r
+ | None ->
+ let ((kn, i) as ind, _), unfolded_c_ty = Tacred.reduce_to_quantified_ind env sigma c_ty in
+ let sort = elimination_sort_of_goal gl in
+ let sigma, elim = Evd.fresh_global env sigma (Indrec.lookup_eliminator env ind sort) in
+ if dir = R2L then sigma, elim else
+ let elim, _ = EConstr.destConst sigma elim in
+ let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in
+ let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in
+ let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in
+ sigma, EConstr.of_constr (mkConst c1')
+ in
let proof = EConstr.mkApp (elim, [| rdx_ty; new_rdx; pred; p; rdx; c |]) in
(* We check the proof is well typed *)
let sigma, proof_ty =
@@ -491,7 +506,8 @@ let rwprocess_rule dir rule gl =
| _ ->
let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in
EConstr.mkApp (pi2, ra), sigma in
- if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.(lib_ref "core.True.type"))) then
+ let sigma,trty = Evd.fresh_global env sigma Coqlib.(lib_ref "core.True.type") in
+ if EConstr.eq_constr sigma a.(0) trty then
let s, sigma = sr sigma 2 in
loop (converse_dir d) sigma s a.(1) rs 0
else
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index 5e600362b4..0ce3752a51 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -391,19 +391,19 @@ Notation "@^~ x" := (fun f => f x) : fun_scope.
Definitions and notation for explicit functions with simplification,
i.e., which simpl and /= beta expand (this is complementary to nosimpl). **)
+#[universes(template)]
+Variant simpl_fun (aT rT : Type) := SimplFun of aT -> rT.
+
Section SimplFun.
Variables aT rT : Type.
-#[universes(template)]
-Variant simpl_fun := SimplFun of aT -> rT.
+Definition fun_of_simpl (f : simpl_fun aT rT) := fun x => let: SimplFun lam := f in lam x.
-Definition fun_of_simpl f := fun x => let: SimplFun lam := f in lam x.
+End SimplFun.
Coercion fun_of_simpl : simpl_fun >-> Funclass.
-End SimplFun.
-
Notation "[ 'fun' : T => E ]" := (SimplFun (fun _ : T => E)) : fun_scope.
Notation "[ 'fun' x => E ]" := (SimplFun (fun x => E)) : fun_scope.
Notation "[ 'fun' x y => E ]" := (fun x => [fun y => E]) : fun_scope.
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index c09250ade5..a1f707ffa8 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -32,7 +32,6 @@ open Ppconstr
open Namegen
open Tactypes
-open Decl_kinds
open Constrexpr
open Constrexpr_ops
@@ -235,7 +234,7 @@ let pr_ssrsimpl _ _ _ = pr_simpl
let wit_ssrsimplrep = add_genarg "ssrsimplrep" (fun env sigma -> pr_simpl)
-let test_ssrslashnum b1 b2 strm =
+let test_ssrslashnum b1 b2 _ strm =
match Util.stream_nth 0 strm with
| Tok.KEYWORD "/" ->
(match Util.stream_nth 1 strm with
@@ -276,8 +275,8 @@ let test_ssrslashnum11 = test_ssrslashnum true true
let test_ssrslashnum01 = test_ssrslashnum false true
let test_ssrslashnum00 = test_ssrslashnum false false
-let negate_parser f x =
- let rc = try Some (f x) with Stream.Failure -> None in
+let negate_parser f tok x =
+ let rc = try Some (f tok x) with Stream.Failure -> None in
match rc with
| None -> ()
| Some _ -> raise Stream.Failure
@@ -385,7 +384,6 @@ open Pltac
ARGUMENT EXTEND ssrindex PRINTED BY { pr_ssrindex }
INTERPRETED BY { interp_index }
-| [ int_or_var(i) ] -> { mk_index ~loc i }
END
@@ -475,7 +473,7 @@ END
(* Old kinds of terms *)
-let input_ssrtermkind strm = match Util.stream_nth 0 strm with
+let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with
| Tok.KEYWORD "(" -> xInParens
| Tok.KEYWORD "@" -> xWithAt
| _ -> xNoFlag
@@ -484,7 +482,7 @@ let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
(* New kinds of terms *)
-let input_term_annotation strm =
+let input_term_annotation _ strm =
match Stream.npeek 2 strm with
| Tok.KEYWORD "(" :: Tok.KEYWORD "(" :: _ -> `DoubleParens
| Tok.KEYWORD "(" :: _ -> `Parens
@@ -523,7 +521,6 @@ ARGUMENT EXTEND ssrterm
GLOBALIZED BY { glob_ssrterm } SUBSTITUTED BY { subst_ssrterm }
RAW_PRINTED BY { pr_ssrterm }
GLOB_PRINTED BY { pr_ssrterm }
-| [ "YouShouldNotTypeThis" constr(c) ] -> { mk_lterm c }
END
GRAMMAR EXTEND Gram
@@ -570,7 +567,6 @@ let pr_ssrbwdview _ _ _ = pr_view
ARGUMENT EXTEND ssrbwdview TYPED AS ssrterm list
PRINTED BY { pr_ssrbwdview }
-| [ "YouShouldNotTypeThis" ] -> { [] }
END
(* Pcoq *)
@@ -594,7 +590,6 @@ let pr_ssrfwdview _ _ _ = pr_view2
ARGUMENT EXTEND ssrfwdview TYPED AS ast_closure_term list
PRINTED BY { pr_ssrfwdview }
-| [ "YouShouldNotTypeThis" ] -> { [] }
END
(* Pcoq *)
@@ -751,7 +746,7 @@ let pushIPatNoop = function
| pats :: orpat -> (IPatNoop :: pats) :: orpat
| [] -> []
-let test_ident_no_do strm =
+let test_ident_no_do _ strm =
match Util.stream_nth 0 strm with
| Tok.IDENT s when s <> "do" -> ()
| _ -> raise Stream.Failure
@@ -762,7 +757,6 @@ let test_ident_no_do =
}
ARGUMENT EXTEND ident_no_do PRINTED BY { fun _ _ _ -> Names.Id.print }
-| [ "YouShouldNotTypeThis" ident(id) ] -> { id }
END
@@ -830,7 +824,7 @@ END
{
-let reject_ssrhid strm =
+let reject_ssrhid _ strm =
match Util.stream_nth 0 strm with
| Tok.KEYWORD "[" ->
(match Util.stream_nth 1 strm with
@@ -840,13 +834,13 @@ let reject_ssrhid strm =
let test_nohidden = Pcoq.Entry.of_parser "test_ssrhid" reject_ssrhid
-let rec reject_binder crossed_paren k s =
+let rec reject_binder crossed_paren k tok s =
match
try Some (Util.stream_nth k s)
with Stream.Failure -> None
with
- | Some (Tok.KEYWORD "(") when not crossed_paren -> reject_binder true (k+1) s
- | Some (Tok.IDENT _) when crossed_paren -> reject_binder true (k+1) s
+ | Some (Tok.KEYWORD "(") when not crossed_paren -> reject_binder true (k+1) tok s
+ | Some (Tok.IDENT _) when crossed_paren -> reject_binder true (k+1) tok s
| Some (Tok.KEYWORD ":" | Tok.KEYWORD ":=") when crossed_paren ->
raise Stream.Failure
| Some (Tok.KEYWORD ")") when crossed_paren -> raise Stream.Failure
@@ -857,7 +851,6 @@ let _test_nobinder = Pcoq.Entry.of_parser "test_nobinder" (reject_binder false 0
}
ARGUMENT EXTEND ssrcpat TYPED AS ssripatrep PRINTED BY { pr_ssripat }
- | [ "YouShouldNotTypeThis" ssriorpat(x) ] -> { IPatCase(Regular x) }
END
(* Pcoq *)
@@ -985,7 +978,6 @@ let pr_ssrintrosarg env sigma _ _ prt (tac, ipats) =
ARGUMENT EXTEND ssrintrosarg TYPED AS (tactic * ssrintros)
PRINTED BY { pr_ssrintrosarg env sigma }
-| [ "YouShouldNotTypeThis" ssrtacarg(arg) ssrintros_ne(ipats) ] -> { arg, ipats }
END
{
@@ -1013,7 +1005,7 @@ END
{
-let accept_ssrfwdid strm =
+let accept_ssrfwdid _ strm =
match stream_nth 0 strm with
| Tok.IDENT id -> accept_before_syms_or_any_id [":"; ":="; "("] strm
| _ -> raise Stream.Failure
@@ -1344,20 +1336,20 @@ ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinde
| [ ssrbvar(bv) ] ->
{ let { CAst.loc=xloc } as x = bvar_lname bv in
(FwdPose, [BFvar]),
- CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) }
+ CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) }
| [ "(" ssrbvar(bv) ")" ] ->
{ let { CAst.loc=xloc } as x = bvar_lname bv in
(FwdPose, [BFvar]),
- CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) }
+ CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) }
| [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] ->
{ let x = bvar_lname bv in
(FwdPose, [BFdecl 1]),
- CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Explicit, t)], mkCHole (Some loc)) }
+ CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Glob_term.Explicit, t)], mkCHole (Some loc)) }
| [ "(" ssrbvar(bv) ne_ssrbvar_list(bvs) ":" lconstr(t) ")" ] ->
{ let xs = List.map bvar_lname (bv :: bvs) in
let n = List.length xs in
(FwdPose, [BFdecl n]),
- CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Explicit, t)], mkCHole (Some loc)) }
+ CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Glob_term.Explicit, t)], mkCHole (Some loc)) }
| [ "(" ssrbvar(id) ":" lconstr(t) ":=" lconstr(v) ")" ] ->
{ (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, Some t, mkCHole (Some loc)) }
| [ "(" ssrbvar(id) ":=" lconstr(v) ")" ] ->
@@ -1369,7 +1361,7 @@ GRAMMAR EXTEND Gram
ssrbinder: [
[ ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" -> {
(FwdPose, [BFvar]),
- CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) } ]
+ CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Glob_term.Explicit,c)],mkCHole (Some loc)) } ]
];
END
@@ -1398,7 +1390,7 @@ let push_binders c2 bs =
let rec fix_binders = let open CAst in function
| (_, { v = CLambdaN ([CLocalAssum(xs, _, t)], _) } ) :: bs ->
- CLocalAssum (xs, Default Explicit, t) :: fix_binders bs
+ CLocalAssum (xs, Default Glob_term.Explicit, t) :: fix_binders bs
| (_, { v = CLetIn (x, v, oty, _) } ) :: bs ->
CLocalDef (x, v, oty) :: fix_binders bs
| _ -> []
@@ -1528,7 +1520,7 @@ let intro_id_to_binder = List.map (function
| IPatId id ->
let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in
(FwdPose, [BFvar]),
- CAst.make @@ CLambdaN ([CLocalAssum([x], Default Explicit, mkCHole xloc)],
+ CAst.make @@ CLambdaN ([CLocalAssum([x], Default Glob_term.Explicit, mkCHole xloc)],
mkCHole None)
| _ -> anomaly "non-id accepted as binder")
@@ -1597,7 +1589,7 @@ END
let sq_brace_tacnames =
["first"; "solve"; "do"; "rewrite"; "have"; "suffices"; "wlog"]
(* "by" is a keyword *)
-let accept_ssrseqvar strm =
+let accept_ssrseqvar _ strm =
match stream_nth 0 strm with
| Tok.IDENT id when not (List.mem id sq_brace_tacnames) ->
accept_before_syms_or_ids ["["] ["first";"last"] strm
@@ -1691,7 +1683,7 @@ let ssr_id_of_string loc s =
^ "Scripts with explicit references to anonymous variables are fragile."))
end; Id.of_string s
-let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ -> ())
+let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ _ -> ())
}
@@ -1711,14 +1703,6 @@ let _ = add_internal_name (is_tagged perm_tag)
(** Tactical extensions. *)
-(* The TACTIC EXTEND facility can't be used for defining new user *)
-(* tacticals, because: *)
-(* - the concrete syntax must start with a fixed string *)
-(* We use the following workaround: *)
-(* - We use the (unparsable) "YouShouldNotTypeThis" token for tacticals that *)
-(* don't start with a token, then redefine the grammar and *)
-(* printer using GEXTEND and set_pr_ssrtac, respectively. *)
-
{
type ssrargfmt = ArgSsr of string | ArgSep of string
@@ -2002,7 +1986,7 @@ END
{
-let accept_ssreqid strm =
+let accept_ssreqid _ strm =
match Util.stream_nth 0 strm with
| Tok.IDENT _ -> accept_before_syms [":"] strm
| Tok.KEYWORD ":" -> ()
@@ -2243,8 +2227,6 @@ END
(** The "congr" tactic *)
-(* type ssrcongrarg = open_constr * (int * constr) *)
-
{
let pr_ssrcongrarg _ _ _ ((n, f), dgens) =
@@ -2423,7 +2405,7 @@ let lbrace = Char.chr 123
(** Workaround to a limitation of coqpp *)
let test_ssr_rw_syntax =
- let test strm =
+ let test _ strm =
if not !ssr_rw_syntax then raise Stream.Failure else
if is_ssr_loaded () then () else
match Util.stream_nth 0 strm with
@@ -2634,7 +2616,7 @@ END
{
-let accept_idcomma strm =
+let accept_idcomma _ strm =
match stream_nth 0 strm with
| Tok.IDENT _ | Tok.KEYWORD "_" -> accept_before_syms [","] strm
| _ -> raise Stream.Failure
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 0adabb0673..064ea0a3e3 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -27,7 +27,6 @@ open Notation_ops
open Notation_term
open Glob_term
open Stdarg
-open Decl_kinds
open Pp
open Ppconstr
open Printer
@@ -280,7 +279,7 @@ let interp_search_notation ?loc tag okey =
Feedback.msg_warning (hov 4 (qtag "In" ++ str "also occurs in " ++ pr_ntns'))
end; ntn
| [ntn] ->
- Feedback.msg_info (hov 4 (qtag "In" ++ str "is part of notation " ++ pr_ntn ntn)); ntn
+ Feedback.msg_notice (hov 4 (qtag "In" ++ str "is part of notation " ++ pr_ntn ntn)); ntn
| ntns' ->
let e = str "occurs in" ++ spc() ++ pr_and_list pr_ntn ntns' in
err (hov 4 (str "ambiguous: " ++ qtag "in" ++ e)) in
@@ -298,7 +297,7 @@ let interp_search_notation ?loc tag okey =
let rbody = glob_constr_of_notation_constr ?loc body in
let m_body = hov 0 (Constrextern.without_symbols prl_glob_constr rbody) in
let m = m_sc ++ pr_ntn ntn_pat ++ spc () ++ str "denotes " ++ m_body in
- Feedback.msg_info (hov 0 m) in
+ Feedback.msg_notice (hov 0 m) in
if List.length !scs > 1 then
let scs' = List.remove (=) sc !scs in
let w = pr_ntn ntn ++ str " is also defined " ++ pr_scs scs' in
@@ -465,7 +464,7 @@ let interp_modloc mr =
let ssrdisplaysearch gr env t =
let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in
- Feedback.msg_info (hov 2 pr_res ++ fnl ())
+ Feedback.msg_notice (hov 2 pr_res ++ fnl ())
}
@@ -560,7 +559,7 @@ END
let print_view_hints env sigma kind l =
let pp_viewname = str "Hint View" ++ pr_viewpos (Some kind) ++ str " " in
let pp_hints = pr_list spc (pr_rawhintref env sigma) l in
- Feedback.msg_info (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ())
+ Feedback.msg_notice (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ())
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 23:15:58 +0000