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 ++++++++++++++++++
 1 file changed, 18 insertions(+)

(limited to 'dev')

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.
-- 
cgit v1.2.3