diff options
Diffstat (limited to 'test-suite/success/Case8.v')
| -rw-r--r-- | test-suite/success/Case8.v | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/test-suite/success/Case8.v b/test-suite/success/Case8.v index b512b5f82..a6113ab9a 100644 --- a/test-suite/success/Case8.v +++ b/test-suite/success/Case8.v @@ -1,7 +1,11 @@ (* 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)). +Inductive t : forall x : 0 = 0, x = x -> Prop := + c : forall 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. +Definition a (x : t _ (refl_equal (refl_equal 0))) := + match x return match x with + | c y => Prop + end with + | c y => y = y + end. |