diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-19 12:19:19 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-19 12:19:19 +0000 |
| commit | 5926ee209a0ad79ca14cf03bc6aadde86e9c35be (patch) | |
| tree | 868af3268833c432dbc0a43ee2dcb667788ea57d /test-suite/success/CasesDep.v | |
| parent | c53748333325f6fb90b09f40ea87c6dbe7142140 (diff) | |
MAJ Grammar
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2338 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/CasesDep.v')
| -rw-r--r-- | test-suite/success/CasesDep.v | 21 |
1 files changed, 10 insertions, 11 deletions
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index 0108c1e94..5cb447f9f 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -46,15 +46,15 @@ Inductive Setoid : Type Definition elem := [A:Setoid] let (S,R,e)=A in S. -Grammar command command1 := - elem [ "|" command0($s) "|"] -> [ <<(elem $s)>>]. +Grammar constr constr1 := + elem [ "|" constr0($s) "|"] -> [ (elem $s) ]. Definition equal := [A:Setoid] <[s:Setoid](Relation |s|)>let (S,R,e)=A in R. -Grammar command command1 := - equal [ command0($c) "=" "%" "S" command0($c2) ] -> - [ <<(equal ? $c $c2)>>]. +Grammar constr constr1 := + equal [ constr0($c) "=" "%" "S" constr0($c2) ] -> + [ (equal ? $c $c2) ]. Axiom prf_equiv : (A:Setoid)(Equivalence |A| (equal A)). @@ -87,9 +87,9 @@ End Maps. Syntactic Definition ap := (explicit_ap ? ?). -Grammar command command8 := - map_setoid [ command7($c1) "=>" command8($c2) ] - -> [ <<(Map_setoid $c1 $c2)>>]. +Grammar constr constr8 := + map_setoid [ constr7($c1) "=>" constr8($c2) ] + -> [ (Map_setoid $c1 $c2) ]. Definition ap2 := [A,B,C:Setoid][f:|(A=>(B=>C))|][a:|A|] (ap (ap f a)). @@ -194,9 +194,8 @@ Parameter t1,t2: TERM. Type Cases t1 t2 of - (var v1) (var v2) => True - - | (oper op1 l1) (oper op2 l2) => False + | (var v1) (var v2) => True + | (oper op1 l1) (oper op2 l2) => False | _ _ => False end. |