From d1bec90c02091858d9d6f5356d43544bfa7fa191 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@bedrocksystems.com>
Date: Tue, 3 May 2022 12:55:01 +0200
Subject: [PATCH] Document reasons for using both `exact` and `refine`.
---
tests/telescopes.v | 3 +++
1 file changed, 3 insertions(+)
diff --git a/tests/telescopes.v b/tests/telescopes.v
index e1836724..d231e291 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -56,6 +56,9 @@ Proof. by rewrite texist_exist. Qed.
(** [tele_arg ..] notation tests.
These tests mainly test type annotations and casts in the [tele_arg]
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].
assert_succeeds exact [tele_arg].
--
GitLab