diff options
Diffstat (limited to 'test-suite/modules/injection_discriminate_inversion.v')
| -rw-r--r-- | test-suite/modules/injection_discriminate_inversion.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/test-suite/modules/injection_discriminate_inversion.v b/test-suite/modules/injection_discriminate_inversion.v index 88c19cb1..d4ac7b3a 100644 --- a/test-suite/modules/injection_discriminate_inversion.v +++ b/test-suite/modules/injection_discriminate_inversion.v @@ -7,18 +7,18 @@ Module M1 := M. Goal forall x, M.C x = M1.C 0 -> x = 0 . intros x H. - (* - injection sur deux constructeurs egaux mais appeles - par des modules differents + (* + injection sur deux constructeurs egaux mais appeles + par des modules differents *) - injection H. + injection H. tauto. Qed. Goal M.C 0 <> M1.C 1. - (* - Discriminate sur deux constructeurs egaux mais appeles - par des modules differents + (* + Discriminate sur deux constructeurs egaux mais appeles + par des modules differents *) intro H;discriminate H. Qed. @@ -26,9 +26,9 @@ Qed. Goal forall x, M.C x = M1.C 0 -> x = 0. intros x H. - (* - inversion sur deux constructeurs egaux mais appeles - par des modules differents + (* + inversion sur deux constructeurs egaux mais appeles + par des modules differents *) inversion H. reflexivity. Qed.
\ No newline at end of file |