Merge PR #10719: Make SSR congr tactic work on arrows in Type.

Reviewed-by: gares

3 files changed, 19 insertions, 2 deletions

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/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