From c9ceeac8f294df6f3b5f01b25141cac17c9a1591 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 11 Jun 2018 18:35:07 +0200
Subject: [ssr] set: merge universe constraints before type checking the term

---
 plugins/ssr/ssrfwd.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 2c046190f4..7fe2421f90 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -47,6 +47,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl =
     let cl = EConstr.Unsafe.to_constr cl in
     try fill_occ_pattern ~raise_NoMatch:true env sigma cl pat occ 1
     with NoMatch -> redex_of_pattern ~resolve_typeclasses:true env pat, cl in
+  let gl = pf_merge_uc ucst gl in
   let c = EConstr.of_constr c in
   let cl = EConstr.of_constr cl in
   if Termops.occur_existential sigma c then errorstrm(str"The pattern"++spc()++
@@ -56,7 +57,6 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl =
   | Cast(t, DEFAULTcast, ty) -> t, (gl, ty)
   | _ -> c, pfe_type_of gl c in
   let cl' = EConstr.mkLetIn (Name id, c, cty, cl) in
-  let gl = pf_merge_uc ucst gl in
   Tacticals.tclTHEN (Proofview.V82.of_tactic (convert_concl cl')) (introid id) gl
 
 open Util
-- 
cgit v1.2.3


From 97485c08cb03987e8d7f2aa98e28510b7187126a Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 11 Jun 2018 18:35:42 +0200
Subject: [ssr] matching: use eq_constr_nounivs in approximated matching

---
 plugins/ssrmatching/ssrmatching.ml4 | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index c20e415b43..9d9b1b2e8c 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -561,8 +561,8 @@ let filter_upat i0 f n u fpats =
   let na = Array.length u.up_a in
   if n < na then fpats else
   let np = match u.up_k with
-  | KpatConst when equal u.up_f f -> na
-  | KpatFixed when equal u.up_f f -> na 
+  | KpatConst when eq_constr_nounivs u.up_f f -> na
+  | KpatFixed when eq_constr_nounivs u.up_f f -> na
   | KpatEvar k when isEvar_k k f -> na
   | KpatLet when isLetIn f -> na
   | KpatLam when isLambda f -> na
@@ -582,8 +582,8 @@ let filter_upat_FO i0 f n u fpats =
   let np = nb_args u.up_FO in
   if n < np then fpats else
   let ok = match u.up_k with
-  | KpatConst -> equal u.up_f f 
-  | KpatFixed -> equal u.up_f f 
+  | KpatConst -> eq_constr_nounivs u.up_f f
+  | KpatFixed -> eq_constr_nounivs u.up_f f
   | KpatEvar k -> isEvar_k k f
   | KpatLet -> isLetIn f
   | KpatLam -> isLambda f
@@ -764,8 +764,8 @@ let mk_tpattern_matcher ?(all_instances=false)
       let match_let f = match kind f with
       | LetIn (_, v, _, b) -> unif_EQ env sigma pv v && unif_EQ env' sigma pb b
       | _ -> false in match_let
-    | KpatFixed -> equal u.up_f
-    | KpatConst -> equal u.up_f
+    | KpatFixed -> eq_constr_nounivs u.up_f
+    | KpatConst -> eq_constr_nounivs u.up_f
     | KpatLam -> fun c ->
        (match kind c with
        | Lambda _ -> unif_EQ env sigma u.up_f c
-- 
cgit v1.2.3