From a4c0127c9cd3c884bf8fd243261798a5f2924bd6 Mon Sep 17 00:00:00 2001 From: barras Date: Wed, 12 Nov 2003 09:34:27 +0000 Subject: petits changements de syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4860 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/g_constrnew.ml4 | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) (limited to 'parsing/g_constrnew.ml4') diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4 index eaf039b9d..cad065329 100644 --- a/parsing/g_constrnew.ml4 +++ b/parsing/g_constrnew.ml4 @@ -79,6 +79,9 @@ let mk_fix(loc,kw,id,dcls) = let fb = List.map mk_cofixb dcls in CCoFix(loc,id,fb) +let mk_single_fix (loc,kw,dcl) = + let (_,id,_,_,_,_) = dcl in mk_fix(loc,kw,id,[dcl]) + let binder_constr = create_constr_entry (get_univ "constr") "binder_constr" @@ -197,12 +200,13 @@ GEXTEND Gram | LocalRawDef ((loc,_),_)::_ -> loc | _ -> dummy_loc in CLetIn(loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2) - | "let"; fx = fix_constr; "in"; c = operconstr LEVEL "200" -> - let (li,id) = match fx with + | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" -> + let fixp = mk_single_fix fx in + let (li,id) = match fixp with CFix(_,id,_) -> id | CCoFix(_,id,_) -> id | _ -> assert false in - CLetIn(loc,(li,Name id),fx,c) + CLetIn(loc,(li,Name id),fixp,c) | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> l | "()" -> []]; po = return_type; ":="; c1 = operconstr LEVEL "200"; "in"; @@ -227,13 +231,15 @@ GEXTEND Gram | "?"; id=ident -> CPatVar(loc,(false,id)) ] ] ; fix_constr: - [ [ kw=fix_kw; dcl=fix_decl -> - let (_,n,_,_,_,_) = dcl in mk_fix(loc,kw,n,[dcl]) - | kw=fix_kw; dcl1=fix_decl; "with"; dcls=LIST1 fix_decl SEP "with"; + [ [ fx1=single_fix -> mk_single_fix fx1 + | (_,kw,dcl1)=single_fix; "with"; dcls=LIST1 fix_decl SEP "with"; "for"; id=identref -> mk_fix(loc,kw,id,dcl1::dcls) ] ] - ; + ; + single_fix: + [ [ kw=fix_kw; dcl=fix_decl -> (loc,kw,dcl) ] ] + ; fix_kw: [ [ "fix" -> true | "cofix" -> false ] ] -- cgit v1.2.3