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/induct.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/induct.v')
| -rw-r--r-- | test-suite/success/induct.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index b24ed2f1b..01ebfc4f0 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -25,7 +25,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 a0) return (P A0 a0) with | refl1 => f end. |