From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- .../modules/injection_discriminate_inversion.v | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'test-suite/modules/injection_discriminate_inversion.v') 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 -- cgit v1.2.3