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.

1 files changed, 18 insertions, 0 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.