From be56f39ecfc0726772cc6930dbc7657348f008e1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 5 May 2020 14:19:04 +0200
Subject: Move the static check of evaluability in unfold tactic to runtime.

See #11840 for a motivation. I had to fix Floats.FloatLemmas because
it uses the same name for a notation and a term, and the fact this
unfold was working on this was clearly a bug. I hope nobody relies
on this kind of stuff in the wild.

Fixes #5764: "Cannot coerce ..." should be a runtime error.
Fixes #5159: "Cannot coerce ..." should not be an error.
Fixes #4925: unfold gives error on Admitted.
---
 test-suite/success/with_strategy.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'test-suite/success')

diff --git a/test-suite/success/with_strategy.v b/test-suite/success/with_strategy.v
index 077b57c87f..6f0833211e 100644
--- a/test-suite/success/with_strategy.v
+++ b/test-suite/success/with_strategy.v
@@ -195,8 +195,8 @@ Opaque F.id.
 
 Goal F.id 0 = F.id 0.
   Fail unfold F.id.
-  (* This should work, but it fails with "Cannot coerce F.id to an evaluable reference." *)
-  Fail F.with_transparent_id ltac:(progress unfold F.id).
+  F.with_transparent_id ltac:(progress unfold F.id).
+  Undo.
   F.with_transparent_id ltac:(let x := constr:(@F.id) in progress unfold x).
 Abort.
 
@@ -212,8 +212,8 @@ Opaque F2.id.
 
 Goal F2.id 0 = F2.id 0.
   Fail unfold F2.id.
-  (* This should work, but it fails with "Cannot coerce F2.id to an evaluable reference." *)
-  Fail F2.with_transparent_id ltac:(progress unfold F2.id).
+  F2.with_transparent_id ltac:(progress unfold F2.id).
+  Undo.
   F2.with_transparent_id ltac:(let x := constr:(@F2.id) in progress unfold x).
 Abort.
 
-- 
cgit v1.2.3