Adapting to current semantics of "simpl non-evaluable-cst"

1 files changed, 2 insertions, 3 deletions

diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v
index 29b91e3aef..b533077962 100644
--- a/test-suite/success/simpl.v
+++ b/test-suite/success/simpl.v
@@ -67,11 +67,10 @@ vm_compute f.
 Fail set (f _).
 Abort.
 
-(* This is a compatibility test with a non evaluable reference, maybe
-   not to be kept for long *)
+(* This is a change wrt 8.4 (waiting to know if it breaks script a lot or not)*)
 
 Goal 0+0=0.
-simpl @eq.
+Fail simpl @eq.
 Abort.
 
 (* Check reference by notation in simpl *)