diff options
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2360.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2360.v b/test-suite/bugs/closed/shouldsucceed/2360.v index b0974a3fdd..4ae97c97bb 100644 --- a/test-suite/bugs/closed/shouldsucceed/2360.v +++ b/test-suite/bugs/closed/shouldsucceed/2360.v @@ -9,5 +9,5 @@ Record Value (etyp : nat -> Type) := Mk { Definition some_value (etyp : nat -> Type) : (Value etyp). Proof. intros. - apply Mk. + Fail apply Mk. (* Check that it does not raise an anomaly *) |