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.ml4
-rw-r--r--plugins/ssr/ssrcommon.mli1
-rw-r--r--plugins/ssr/ssreflect.v1
-rw-r--r--plugins/ssr/ssrequality.ml16
-rw-r--r--plugins/ssr/ssrfun.v10
-rw-r--r--plugins/ssr/ssrvernac.mlg8
7 files changed, 28 insertions, 20 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 473612fda7..dbb60e6712 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -680,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 4c6b7cdcb6..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)));
@@ -134,10 +139,17 @@ let newssrcongrtac arg ist gl =
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
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/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index f3f1d713e9..064ea0a3e3 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -279,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
@@ -297,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
@@ -464,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 ())
}
@@ -559,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-02 02:25:41 +0000