Skip to content
Snippets Groups Projects
Commit d1bec90c authored by Jan-Oliver Kaiser's avatar Jan-Oliver Kaiser
Browse files

Document reasons for using both `exact` and `refine`.

parent 0ab4fb1e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 3 additions and 0 deletions
tests/telescopes.v
+ 3
− 0
View file @ d1bec90c
...@@ -56,6 +56,9 @@ Proof. by rewrite texist_exist. Qed. ...@@ -56,6 +56,9 @@ Proof. by rewrite texist_exist. Qed.
(** [tele_arg ..] notation tests. (** [tele_arg ..] notation tests.
These tests mainly test type annotations and casts in the [tele_arg] These tests mainly test type annotations and casts in the [tele_arg]
notations. notations.
We test that Coq can typecheck literal telescope arguments in two ways:
- tactic unification/old unification using [exact]
- evarconv/new unification using [refine]
*) *)
Example tele_arg_notation_0 : [tele]. Example tele_arg_notation_0 : [tele].
assert_succeeds exact [tele_arg]. assert_succeeds exact [tele_arg].
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment