From 14c940b332512f313b0b80acd6a17f80721b32fc Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 24 Aug 2015 07:53:57 +0200
Subject: Compare pattern heads (constants) up to "univs"

So that Universe Polymorphic constants are compared "correctly",
i.e. not discriminated by the pattern filtering phase (verbatim
head comparison) but eventually by unification.
---
 mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'mathcomp/ssreflect/plugin')

diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
index effd193..c47c946 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
+++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
@@ -537,8 +537,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 Term.eq_constr u.up_f f -> na
-  | KpatFixed when Term.eq_constr u.up_f f -> na 
+  | KpatConst when Term.eq_constr_nounivs u.up_f f -> na
+  | KpatFixed when Term.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
@@ -554,8 +554,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 -> Term.eq_constr u.up_f f 
-  | KpatFixed -> Term.eq_constr u.up_f f 
+  | KpatConst -> Term.eq_constr_nounivs u.up_f f
+  | KpatFixed -> Term.eq_constr_nounivs u.up_f f
   | KpatEvar k -> isEvar_k k f
   | KpatLet -> isLetIn f
   | KpatLam -> isLambda f
-- 
cgit v1.2.3