petits changements de syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4860 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 49 insertions, 49 deletions

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 ] ]
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index 5a1f13132..aaf31da53 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -94,9 +94,9 @@ GEXTEND Gram
           body = tactic_expr -> TacLetRecIn (rcl,body)
       | "let"; llc = LIST1 let_clause SEP "with"; "in";
           u = tactic_expr -> TacLetIn (make_letin_clause loc llc,u)
-      | "match"; IDENT "context"; "with"; mrl = match_context_list; "end" ->
+      | "match"; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
           TacMatchContext (false,mrl)
-      | "match"; IDENT "reverse"; IDENT "context"; "with";
+      | "match"; IDENT "reverse"; IDENT "goal"; "with";
         mrl = match_context_list; "end" ->
           TacMatchContext (true,mrl)
       |	"match"; c = tactic_expr; "with"; mrl = match_list; "end" ->
@@ -114,15 +114,9 @@ GEXTEND Gram
       | IDENT "fail"; n = [ n = natural -> n | -> fail_default_value ];
 	  s = [ s = STRING -> s | -> ""] -> TacFail (n,s)
       | st = simple_tactic -> TacAtom (loc,st)
-      | IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
-	  TacArg(ConstrMayEval (ConstrEval (rtc,c)))
-      | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" ->
-	  TacArg(ConstrMayEval (ConstrContext (id,c)))
-      | IDENT "check"; c = Constr.constr ->
-	  TacArg(ConstrMayEval (ConstrTypeOf c))
-      | IDENT "fresh"; s = OPT STRING ->
-	  TacArg (TacFreshId s)
-      | "'"; c = Constr.constr -> TacArg(ConstrMayEval(ConstrTerm c))
+      | a = may_eval_arg -> TacArg(a)
+      | IDENT"constr"; ":"; c = Constr.constr ->
+          TacArg(ConstrMayEval(ConstrTerm c))
       | r = reference; la = LIST1 tactic_arg ->
           TacArg(TacCall (loc,r,la))
       | r = reference -> TacArg (Reference r) ]
@@ -132,10 +126,21 @@ GEXTEND Gram
   ;
   (* Tactic arguments *)
   tactic_arg:
-    [ [ "'"; a = tactic_expr LEVEL "0" -> arg_of_expr a
+    [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> arg_of_expr a
+      | a = may_eval_arg -> a
       | a = tactic_atom -> a
       | c = Constr.constr -> ConstrMayEval (ConstrTerm c) ] ]
   ;
+  may_eval_arg:
+    [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
+	  ConstrMayEval (ConstrEval (rtc,c))
+      | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" ->
+	  ConstrMayEval (ConstrContext (id,c))
+      | IDENT "type"; "of"; c = Constr.constr ->
+	  ConstrMayEval (ConstrTypeOf c)
+      | IDENT "fresh"; s = OPT STRING ->
+	  TacFreshId s ] ]
+  ;
   tactic_atom:
     [ [ id = METAIDENT -> MetaIdArg (loc,id)
       | r = reference -> Reference r
@@ -149,13 +154,7 @@ GEXTEND Gram
     [ [ id = identref; ":="; te = tactic_expr ->
           LETCLAUSE (id, None, arg_of_expr te)
       | id = identref; args = LIST1 input_fun; ":="; te = tactic_expr ->
-          LETCLAUSE (id, None, arg_of_expr (TacFun(args,te)))
-      | (_,id) = identref; ":"; c = Constr.lconstr; ":="; IDENT "proof" ->
-          LETTOPCLAUSE (id, c)
-      | id = identref; ":"; c = tactic_expr; ":="; te = tactic_expr ->
-          LETCLAUSE (id, Some c, arg_of_expr te)
-      |	(_,id) = identref; ":"; c = Constr.constr ->
-	  LETTOPCLAUSE (id, c) ] ]
+          LETCLAUSE (id, None, arg_of_expr (TacFun(args,te))) ] ]
   ;
   rec_clause:
     [ [ name = identref; it = LIST1 input_fun; ":="; body = tactic_expr ->
@@ -173,6 +172,8 @@ GEXTEND Gram
   match_context_rule:
     [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
         "=>"; te = tactic_expr -> Pat (largs, mp, te)
+      | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
+        "]"; "=>"; te = tactic_expr -> Pat (largs, mp, te)
       | "_"; "=>"; te = tactic_expr -> All te ] ]
   ;
   match_context_list:
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 29dc5cfba..54af7a4f2 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -127,7 +127,7 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
 
 if not !Options.v7 then
 GEXTEND Gram
-  GLOBAL: simple_tactic constrarg constr_with_bindings quantified_hypothesis
+  GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
     red_expr int_or_var castedopenconstr;
 
   int_or_var:
@@ -163,14 +163,6 @@ GEXTEND Gram
       |	id = METAIDENT -> MetaId (loc,id)
       ] ]
   ;
-  constrarg:
-    [ [ IDENT "inst"; id = identref; "["; c = Constr.lconstr; "]" ->
-        ConstrContext (id, c)
-      | IDENT "eval"; rtc = Tactic.red_expr; "in"; c = Constr.constr ->
-        ConstrEval (rtc,c) 
-      | IDENT "check"; c = Constr.constr -> ConstrTypeOf c
-      | c = Constr.constr -> ConstrTerm c ] ]
-  ;
   castedopenconstr:
     [ [ c = constr -> c ] ]
   ;
@@ -186,11 +178,16 @@ GEXTEND Gram
   conversion:
     [ [ c = constr -> (None, c)
       | c1 = constr; "with"; c2 = constr -> (Some ([],c1), c2)
-      | c1 = constr; IDENT "at"; nl = LIST1 integer; "with"; c2 = constr ->
+      | c1 = constr; "at"; nl = LIST1 integer; "with"; c2 = constr ->
 	  (Some (nl,c1), c2) ] ]
   ;
   pattern_occ:
-    [ [ c = constr; nl = LIST0 integer -> (nl,c) ] ]
+    [ [ c = constr; "at"; nl = LIST0 integer -> (nl,c)
+      | c = constr -> ([],c) ] ]
+  ;
+  unfold_occ:
+    [ [ c = global; "at"; nl = LIST0 integer -> (nl,c)
+      | c = global -> ([],c) ] ]
   ;
   pattern_occ_hyp_tail_list:
     [ [ pl = pattern_occ_hyp_list -> pl | -> (None,[]) ] ]
@@ -231,9 +228,6 @@ GEXTEND Gram
   with_binding_list:
     [ [ "with"; bl = binding_list -> bl | -> NoBindings ] ]
   ;
-  unfold_occ:
-    [ [ c = global; nl = LIST0 integer -> (nl,c) ] ]
-  ;
   red_flag:
     [ [ IDENT "beta" -> FBeta
       | IDENT "delta" -> FDeltaBut []
@@ -252,7 +246,7 @@ GEXTEND Gram
       | IDENT "compute" -> Cbv (make_red_flag [FBeta;FIota;FDeltaBut [];FZeta])
       | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
       | IDENT "fold"; cl = LIST1 constr -> Fold cl
-      | IDENT "pattern"; pl = LIST1 pattern_occ SEP "," -> Pattern pl ] ]
+      | IDENT "pattern"; pl = LIST1 pattern_occ SEP","-> Pattern pl ] ]
   ;
   (* This is [red_tactic] including possible extensions *)
   red_expr:
@@ -394,8 +388,8 @@ GEXTEND Gram
       | IDENT "left"; bl = with_binding_list -> TacLeft bl
       | IDENT "right"; bl = with_binding_list -> TacRight bl
       | IDENT "split"; bl = with_binding_list -> TacSplit (false,bl)
-      | IDENT "exists"; bl = binding_list -> TacSplit (true,bl)
-      | IDENT "exists" -> TacSplit (true,NoBindings)
+      | "exists"; bl = binding_list -> TacSplit (true,bl)
+      | "exists" -> TacSplit (true,NoBindings)
       | IDENT "constructor"; n = num_or_meta; l = with_binding_list ->
 	  TacConstructor (n,l)
       | IDENT "constructor"; t = OPT tactic -> TacAnyConstructor t
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 05aea1015..91e765dc4 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -28,7 +28,7 @@ open Vernac_
 open Module
 
 
-let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "..."; "where" ]
+let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "..."; "where"; "at" ]
 let _ = 
   if not !Options.v7 then
     List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw
@@ -337,8 +337,7 @@ GEXTEND Gram
   export_token:
     [ [ IDENT "Import" -> Some false
       | IDENT "Export" -> Some true
-      | IDENT "Closed" -> None
-      |  -> Some false ] ]
+      |  -> None ] ]
   ;
   specif_token:
     [ [ IDENT "Implementation" -> Some false
@@ -723,10 +722,10 @@ GEXTEND Gram
       | IDENT "next"; IDENT "level" -> NextLevel ] ]
   ;
   syntax_modifier:
-    [ [ x = IDENT; IDENT "at"; lev = level -> SetItemLevel ([x],lev)
-      | x = IDENT; ","; l = LIST1 IDENT SEP ","; IDENT "at"; 
+    [ [ x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev)
+      | x = IDENT; ","; l = LIST1 IDENT SEP ","; "at"; 
         lev = level -> SetItemLevel (x::l,lev)
-      | IDENT "at"; IDENT "level"; n = natural -> SetLevel n
+      | "at"; IDENT "level"; n = natural -> SetLevel n
       | IDENT "left"; IDENT "associativity" -> SetAssoc Gramext.LeftA
       | IDENT "right"; IDENT "associativity" -> SetAssoc Gramext.RightA
       | IDENT "no"; IDENT "associativity" -> SetAssoc Gramext.NonA