diff options
| -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. |