diff options
| author | filliatr | 1999-09-08 13:54:35 +0000 |
|---|---|---|
| committer | filliatr | 1999-09-08 13:54:35 +0000 |
| commit | cfba911ee7f12c68e24b2d8db2cee08d6c6713ff (patch) | |
| tree | 79bc8e510194dad127dbc818624dc8501be75d33 /parsing/g_multiple_case.ml4 | |
| parent | 6560ae848fbc6a60e432d48d85fbbf12a8d2e6aa (diff) | |
compilation des grammaires (ouf)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@57 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_multiple_case.ml4')
| -rw-r--r-- | parsing/g_multiple_case.ml4 | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/parsing/g_multiple_case.ml4 b/parsing/g_multiple_case.ml4 index 4c20e3a279..6611911cad 100644 --- a/parsing/g_multiple_case.ml4 +++ b/parsing/g_multiple_case.ml4 @@ -8,7 +8,7 @@ open Command GEXTEND Gram pattern_list: [ [ -> ([],[]) - | (id1,p) = pattern; (id2,pl) = pattern_list -> (id1@id2,[p :: pl]) ] ] + | (id1,p) = pattern; (id2,pl) = pattern_list -> (id1@id2, p::pl) ] ] ; lsimple_pattern: [ [ c = simple_pattern2 -> c ] ] @@ -20,7 +20,7 @@ GEXTEND Gram simple_pattern_list: [ [ -> ([],[]) | (id1,p) = simple_pattern; (id2,pl) = simple_pattern_list -> - (id1@id2,[p :: pl]) ] ] + (id1@id2, p::pl) ] ] ; (* The XTRA"!" means we want to override the implicit arg mecanism of bdize, since params are not given in patterns *) @@ -28,7 +28,7 @@ GEXTEND Gram [ [ (id1,p) = simple_pattern; (id2,lp) = pattern_list -> (id1@id2, <:ast< (APPLIST (XTRA "!" $p) ($LIST $lp)) >>) | (id1,p) = simple_pattern; "as"; id = ident -> - ([Ast.nvar_of_ast id::id1], <:ast< (XTRA"AS" $id $p) >>) + ((Ast.nvar_of_ast id)::id1, <:ast< (XTRA"AS" $id $p) >>) | (id1,c1) = simple_pattern; ","; (id2,c2) = simple_pattern -> (id1@id2, <:ast< (APPLIST (XTRA "!" pair) $c1 $c2) >>) ] ] ; @@ -37,20 +37,20 @@ GEXTEND Gram ; ne_pattern_list: [ [ (id1,c1) = pattern; (id2,cl) = ne_pattern_list -> - (id1@id2, [c1 :: cl]) + (id1@id2, c1::cl) | (id1,c1) = pattern -> (id1,[c1]) ] ] ; equation: [ [ (ids,lhs) = ne_pattern_list; "=>"; rhs = command -> let br = - List.fold_right (fun s ast -> CoqAst.Slam loc (Some s) ast) + List.fold_right (fun s ast -> Coqast.Slam loc (Some s) ast) ids <:ast< (XTRA"EQN" $rhs ($LIST $lhs)) >> in - let lid = List.map (fun s -> CoqAst.Id loc s) ids in + let lid = List.map (fun s -> Coqast.Id loc s) ids in <:ast< (XTRA"LAMEQN"($LIST $lid) $br) >> ] ] ; ne_eqn_list: - [ [ e = equation; "|"; leqn = ne_eqn_list -> [e :: leqn] + [ [ e = equation; "|"; leqn = ne_eqn_list -> e :: leqn | e = equation -> [e] ] ] ; |