diff options
author | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-02 22:30:42 +0000 |
---|---|---|
committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-02 22:30:42 +0000 |
commit | c2dda7cf57f29e5746e5903c310a7ce88525909c (patch) | |
tree | aa60a6f57014c20f980e90230b122cc76ba21e9b /test-suite/success/Inductive.v | |
parent | 401f17afa2e9cc3f2d734aef0d71a2c363838ebd (diff) |
"Let in" in pattern hell, one more iteration
This reverts commit 28bcf05dd876beea8697f6ee47ebf916a8b94cdf.
An other wrong externalize function
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15021 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/Inductive.v')
-rw-r--r-- | test-suite/success/Inductive.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index da5dd5e40..59aa87de4 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -17,7 +17,7 @@ Check fun (P : forall A : Type, let B := A in A -> Type) (f : P True I) (A : Type) => let B := A in fun (a : A) (e : eq1 A a) => - match e in (eq1 A0 B0 a0) return (P A0 a0) with + match e in (@eq1 A0 B0 a0) return (P A0 a0) with | refl1 => f end. @@ -37,7 +37,7 @@ Check fun (x y : E -> F) (P : forall c : C, A C D x y c -> Type) (f : forall z : C, P z (I C D x y z)) (y0 : C) (a : A C D x y y0) => - match a as a0 in (A _ _ _ _ _ _ y1) return (P y1 a0) with + match a as a0 in (A _ _ _ _ y1) return (P y1 a0) with | I x0 => f x0 end). |