diff options
Diffstat (limited to 'test-suite/success/Inversion.v')
| -rw-r--r-- | test-suite/success/Inversion.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index 45c71615..ee540d71 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -31,7 +31,7 @@ Inductive in_extension (I : Set) (r : rule I) : extension I -> Type := | in_first : forall e, in_extension r (add_rule r e) | in_rest : forall e r', in_extension r e -> in_extension r (add_rule r' e). -Implicit Arguments NL [I]. +Arguments NL [I]. Inductive super_extension (I : Set) (e : extension I) : extension I -> Type := @@ -107,6 +107,7 @@ Goal forall o, foo2 o -> 0 = 1. intros. eapply trans_eq. inversion H. +Abort. (* Check that the part of "injection" that is called by "inversion" does the same number of intros as the number of equations @@ -136,6 +137,7 @@ Goal True -> True. intro. Fail inversion H using False. Fail inversion foo using True_ind. +Abort. (* Was failing at some time between 7 and 10 September 2014 *) (* even though, it is not clear that the resulting context is interesting *) |