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.

---
 dev/doc/univpoly.txt                  | 18 ++++++++++++++++++
 pretyping/constrMatching.ml           |  2 +-
 test-suite/bugs/closed/HoTT_coq_052.v | 23 +++++++++++++++++++++++
 test-suite/bugs/opened/HoTT_coq_052.v | 22 ----------------------
 4 files changed, 42 insertions(+), 23 deletions(-)
 create mode 100644 test-suite/bugs/closed/HoTT_coq_052.v
 delete mode 100644 test-suite/bugs/opened/HoTT_coq_052.v

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/closed/HoTT_coq_052.v b/test-suite/bugs/closed/HoTT_coq_052.v
new file mode 100644
index 0000000000..3fc663c6be
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_052.v
@@ -0,0 +1,23 @@
+Goal Type = Type.
+  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 match goal with |- ?x = ?x => idtac x end.
+Abort.
+
+Goal Type = Prop.
+  (* This should fail *)
+  Fail match goal with |- ?x = ?x => idtac end.
+Abort.
+
+Goal Type = Set.
+  (* This should fail *)
+  Fail match goal with |- ?x = ?x => idtac end.
+Abort.
diff --git a/test-suite/bugs/opened/HoTT_coq_052.v b/test-suite/bugs/opened/HoTT_coq_052.v
deleted file mode 100644
index 886dbad9ef..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_052.v
+++ /dev/null
@@ -1,22 +0,0 @@
-Goal Type = Type.
-  match goal with |- ?x = ?x => 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.
-Abort.
-
-Goal Type = Prop.
-  (* This should fail *)
-  Fail Fail match goal with |- ?x = ?x => idtac end.
-Abort.
-
-Goal Type = Set.
-  (* This should fail *)
-  Fail Fail match goal with |- ?x = ?x => idtac end.
-Abort.
-- 
cgit v1.2.3