From a0141c0ccc295af0d7938e8e515c9eef40449d73 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 15 Jun 2014 14:15:30 +0200
Subject: Change Ltac constr matching semantics to consider universes when
 merging two bindings of the same variable (fixing HoTT bug #52). Document the
 unification of universes in Ltac/tactics.

---
 pretyping/constrMatching.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/constrMatching.ml b/pretyping/constrMatching.ml
index 243b563d36..21e22e0bbf 100644
--- a/pretyping/constrMatching.ml
+++ b/pretyping/constrMatching.ml
@@ -63,7 +63,7 @@ let warn_bound_again name =
 let constrain n (ids, m as x) (names, terms as subst) =
   try
     let (ids', m') = Id.Map.find n terms in
-    if List.equal Id.equal ids ids' && eq_constr_nounivs m m' then subst
+    if List.equal Id.equal ids ids' && eq_constr m m' then subst
     else raise PatternMatchingFailure
   with Not_found ->
     let () = if Id.Map.mem n names then warn_bound_meta n in
-- 
cgit v1.2.3