diff options
Diffstat (limited to 'test-suite/success/Case10.v')
| -rw-r--r-- | test-suite/success/Case10.v | 34 |
1 files changed, 18 insertions, 16 deletions
diff --git a/test-suite/success/Case10.v b/test-suite/success/Case10.v index 73413c47..378859e9 100644 --- a/test-suite/success/Case10.v +++ b/test-suite/success/Case10.v @@ -2,25 +2,27 @@ (* To test compilation of dependent case *) (* Multiple Patterns *) (* ============================================== *) -Inductive skel: Type := - PROP: skel - | PROD: skel->skel->skel. +Inductive skel : Type := + | PROP : skel + | PROD : skel -> skel -> skel. Parameter Can : skel -> Type. -Parameter default_can : (s:skel) (Can s). +Parameter default_can : forall s : skel, Can s. -Type [s1,s2:skel] - <[s1,_:skel](Can s1)>Cases s1 s2 of - PROP PROP => (default_can PROP) - | s1 _ => (default_can s1) - end. +Type + (fun s1 s2 : skel => + match s1, s2 return (Can s1) with + | PROP, PROP => default_can PROP + | s1, _ => default_can s1 + end). -Type [s1,s2:skel] -<[s1:skel][_:skel](Can s1)>Cases s1 s2 of - PROP PROP => (default_can PROP) -| (PROP as s) _ => (default_can s) -| ((PROD s1 s2) as s) PROP => (default_can s) -| ((PROD s1 s2) as s) _ => (default_can s) -end. +Type + (fun s1 s2 : skel => + match s1, s2 return (Can s1) with + | PROP, PROP => default_can PROP + | PROP as s, _ => default_can s + | PROD s1 s2 as s, PROP => default_can s + | PROD s1 s2 as s, _ => default_can s + end). |