From f76dc3d0a3e677e6e93f60adbc7522d23aa12654 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 9 Nov 2008 21:09:24 +0000
Subject: - Correction erreur dans test output Notation.v - Ajout test pour
 non-régression du bug #1968

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11569 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/Notations.v  | 2 ++
 test-suite/success/Inversion.v | 8 ++++++++
 2 files changed, 10 insertions(+)

diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 4577f0e196..b37c3638af 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -145,6 +145,8 @@ Check (false && I 3)%bool /\ I 6.
 (**********************************************************************)
 (* Check notations with several recursive patterns                    *)
 
+Open Scope Z_scope.
+
 Notation "[| x , y , .. , z ; a , b , .. , c |]" :=
   (pair (pair .. (pair x y) .. z) (pair .. (pair a b) .. c)).
 Check [|1,2,3;4,5,6|].
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index f83328e822..54b03b3eba 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -99,3 +99,11 @@ Lemma depinv : forall a b, foo a b -> True.
 intros a b H.
 inversion H.
 Abort.
+
+(* Check non-regression of bug #1968 *)
+
+Inductive foo : option nat -> Prop := Foo : forall t, foo (Some t).
+Goal forall o, foo o -> 0 = 1.
+intros.
+eapply trans_eq. 
+inversion H.
-- 
cgit v1.2.3