diff options
| author | Matthieu Sozeau | 2016-07-27 18:26:42 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-07-29 19:35:25 +0200 |
| commit | 9f5e248704f1574b0acbb9bddd287e40daac8727 (patch) | |
| tree | 18325ccd1644df6d265c1d5dfda168a1f6a42fff /test-suite | |
| parent | 25ef9dda0311213bb2f6e2b9cd0b87be2128599b (diff) | |
Fix bug #3886, generation of obligations of fixes
This partially reverts c14ccd1b8a3855d4eb369be311d4b36a355e46c1
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/3886.v | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3886.v b/test-suite/bugs/closed/3886.v new file mode 100644 index 0000000000..2ac4abe54f --- /dev/null +++ b/test-suite/bugs/closed/3886.v @@ -0,0 +1,23 @@ +Require Import Program. + +Inductive Even : nat -> Prop := +| evenO : Even O +| evenS : forall n, Odd n -> Even (S n) +with Odd : nat -> Prop := +| oddS : forall n, Even n -> Odd (S n). + +Program Fixpoint doubleE {n} (e : Even n) : Even (2 * n) + := _ +with doubleO {n} (o : Odd n) : Odd (S (2 * n)) + := _. +Obligations. +Axiom cheat : forall {A}, A. +Obligation 1 of doubleE. +apply cheat. +Qed. + +Obligation 1 of doubleO. +apply cheat. +Qed. + +Check doubleE.
\ No newline at end of file |