diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-03 20:25:07 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-03 20:25:07 +0000 |
| commit | 4fabc4b3db8589597ea289e8f93f8bf25445bc9f (patch) | |
| tree | 0838f2e5f94aeae800fdb6e4531187fb5a44cb4f | |
| parent | a5cb08bd2d8acf5da488131f7e7f387a26ba27ed (diff) | |
Was failing in 8.0pl1
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6393 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | test-suite/success/Case8.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/success/Case8.v b/test-suite/success/Case8.v new file mode 100644 index 000000000..b512b5f82 --- /dev/null +++ b/test-suite/success/Case8.v @@ -0,0 +1,7 @@ +(* Check dependencies in the matching predicate (was failing in V8.0pl1) *) + +Inductive t : (x:O=O) x=x -> Prop := + c : (x:0=0) (t x (refl_equal ? x)). + +Definition a [x:(t ? (refl_equal ? (refl_equal ? O)))] := + <[_;_;x]Cases x of (c y) => Prop end>Cases x of (c y) => y=y end. |