diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-11 23:07:14 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-18 14:16:33 +0200 |
| commit | 89a85a6603b7112e685a052d728284d3e4c2881e (patch) | |
| tree | f3a3c51bd32439eeab9c2138d45a115adffa7850 /doc | |
| parent | 0daf6af5949dbc7304e9fc3adf063519d5a60c4b (diff) | |
Fix #7421: constr_eq ignores universe constraints.
The test isn't quite the one in #7421 because that use of algebraic
universes is wrong.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 29c2f8b81..d0a0d568e 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3949,9 +3949,20 @@ succeeds, and results in an error otherwise. :name: constr_eq This tactic checks whether its arguments are equal modulo alpha - conversion and casts. + conversion, casts and universe constraints. It may unify universes. .. exn:: Not equal. +.. exn:: Not equal (due to universes). + +.. tacn:: constr_eq_strict @term @term + :name: constr_eq_strict + + This tactic checks whether its arguments are equal modulo alpha + conversion, casts and universe constraints. It does not add new + constraints. + +.. exn:: Not equal. +.. exn:: Not equal (due to universes). .. tacn:: unify @term @term :name: unify |