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.

3 files changed, 24 insertions, 5 deletions

diff --git a/dev/doc/univpoly.txt b/dev/doc/univpoly.txt
index ad0fd9eb22..4c89af01db 100644
--- a/dev/doc/univpoly.txt
+++ b/dev/doc/univpoly.txt
@@ -235,3 +235,21 @@ typing constraint. Adding the correct type annotations will always fix
 this.
 
 
+Unification semantics
+=====================
+
+In Ltac, matching with:
+
+- a universe polymorphic constant [c] matches any instance of the
+  constant.
+- a variable ?x already bound to a term [t] (non-linear pattern) uses 
+  strict equality of universes (e.g., Type@{i} and Type@{j} are not
+  equal).
+
+In tactics:
+
+- [change foo with bar], [pattern foo] will unify all instances of [foo]
+  (and convert them with [bar]). This might incur unifications of
+  universes. [change] uses conversion while [pattern] only does
+  syntactic matching up-to unification of universes.
+- [apply], [refine] use unification up to universes.
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
diff --git a/test-suite/bugs/opened/HoTT_coq_052.v b/test-suite/bugs/closed/HoTT_coq_052.v
index 886dbad9ef..3fc663c6be 100644
--- a/test-suite/bugs/opened/HoTT_coq_052.v
+++ b/test-suite/bugs/closed/HoTT_coq_052.v
@@ -1,22 +1,23 @@
 Goal Type = Type.
-  match goal with |- ?x = ?x => idtac end.
+  match goal with |- ?x = ?y => idtac end.
 Abort.
 
 Goal Prop.
   Fail match goal with |- Type => idtac end.
 Abort.
 
+
 Goal Prop = Set.
   (* This should fail *)
-  Fail Fail match goal with |- ?x = ?x => idtac end.
+ Fail match goal with |- ?x = ?x => idtac x end.
 Abort.
 
 Goal Type = Prop.
   (* This should fail *)
-  Fail Fail match goal with |- ?x = ?x => idtac end.
+  Fail match goal with |- ?x = ?x => idtac end.
 Abort.
 
 Goal Type = Set.
   (* This should fail *)
-  Fail Fail match goal with |- ?x = ?x => idtac end.
+  Fail match goal with |- ?x = ?x => idtac end.
 Abort.