diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-16 18:32:23 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-16 18:32:23 +0000 |
| commit | ded597434229e373243f8d320ce51aaa4e35981f (patch) | |
| tree | f3ff61a8ac2fa445a642eaf574d2b562126dcd1f /parsing | |
| parent | a69a28443fad9374d6ac9f3fe02d0270577fdba6 (diff) | |
lettac -> set
suppression de la notation carre de R
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4659 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tacticnew.ml4 | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4 index fa9a402eb..bba623da3 100644 --- a/parsing/g_tacticnew.ml4 +++ b/parsing/g_tacticnew.ml4 @@ -280,8 +280,8 @@ GEXTEND Gram | -> [] ] ] ; fixdecl: - [ [ id = base_ident; bl=LIST0 Constr.binder; ann=fixannot; - ":"; ty=lconstr -> (loc,id,bl,ann,ty) ] ] + [ [ "("; id = base_ident; bl=LIST0 Constr.binder; ann=fixannot; + ":"; ty=lconstr; ")" -> (loc,id,bl,ann,ty) ] ] ; fixannot: [ [ "{"; IDENT "struct"; id=name; "}" -> Some id @@ -323,11 +323,11 @@ GEXTEND Gram | IDENT "casetype"; c = constr -> TacCaseType c | "fix"; n = natural -> TacFix (None,n) | "fix"; id = base_ident; n = natural -> TacFix (Some id,n) - | "fix"; id = base_ident; n = natural; "with"; fd = LIST0 fixdecl -> + | "fix"; id = base_ident; n = natural; "with"; fd = LIST1 fixdecl -> TacMutualFix (id,n,List.map mk_fix_tac fd) | "cofix" -> TacCofix None | "cofix"; id = base_ident -> TacCofix (Some id) - | "cofix"; id = base_ident; "with"; fd = LIST0 fixdecl -> + | "cofix"; id = base_ident; "with"; fd = LIST1 fixdecl -> TacMutualCofix (id,List.map mk_cofix_tac fd) | IDENT "cut"; c = constr -> TacCut c @@ -342,7 +342,7 @@ GEXTEND Gram | IDENT "generalize"; lc = LIST1 constr -> TacGeneralize lc | IDENT "generalize"; IDENT "dependent"; c = constr -> TacGeneralizeDep c - | IDENT "lettac"; "("; id = base_ident; ":="; c = lconstr; ")"; + | IDENT "set"; "("; id = base_ident; ":="; c = lconstr; ")"; p = clause_pattern -> TacLetTac (id,c,p) | IDENT "instantiate"; "("; n = natural; ":="; c = lconstr; ")" -> TacInstantiate (n,c) |