From 2352d3a9763074d1ffea5be7bd019ed41ca66f1a Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 18 Dec 2017 19:32:28 +0100
Subject: [PATCH] Documentation.
---
theories/proofmode/tactics.v | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 64b281c78..ff7858d03 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -85,6 +85,12 @@ Tactic Notation "iStartProof" uconstr(PROP) :=
| |- @envs_entails ?PROP' _ _ =>
let x := type_term (eq_refl : @eq Type PROP PROP') in idtac
| |- let _ := _ in _ => fail
+
+ (* We eta-expand [as_valid_2], in order to make sure that
+ [iStartProof works] even if [PROP] is the carrier type. In this
+ case, typing this expression will end up unifying PROP with
+ [bi_car _], and hence trigger the canonical structures mechanism
+ to find the corresponding bi. *)
| |- ?φ => eapply (λ P : PROP, @as_valid_2 φ _ P);
[apply _ || fail "iStartProof: not a Bi entailment"
|apply tac_adequate]
--
GitLab