aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/success/evars.v4
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 21c72475ed..f42c6a036e 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -404,3 +404,7 @@ Abort.
not strict enough evar restriction) *)
Check match Some _ with None => _ | _ => _ end.
+
+(* Used to fail for a couple of days in Nov 2014 *)
+
+Axiom test : forall P1 P2, P1 = P2 -> P1 -> P2.