From f3033b7d0a69d85019ee9228c739ac71afc0bb63 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 15 Feb 2018 18:31:05 +0100
Subject: [PATCH] Add back cbv zeta in iIntoValid.
---
theories/proofmode/tactics.v | 5 ++++-
1 file changed, 4 insertions(+), 1 deletion(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index cf98dc70b..bb779984e 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -621,7 +621,10 @@ a goal [P] for non-dependent arguments [x_i : P]. *)
Tactic Notation "iIntoValid" open_constr(t) :=
let rec go t :=
let tT := type of t in
- lazymatch tT with
+ let tT := eval cbv zeta in tT in (* In the case tT contains let-bindings. *)
+ lazymatch tT with (* We do not use hnf of tT, because, if
+ entailment is not opaque, then it would
+ unfold it. *)
| ?P → ?Q => let H := fresh in assert P as H; [|go uconstr:(t H); clear H]
| ∀ _ : ?T, _ =>
(* Put [T] inside an [id] to avoid TC inference from being invoked. *)
--
GitLab