nouvelle syntaxe de ltac

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

4 files changed, 19 insertions, 46 deletions

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index b342d9716..41ee54ea4 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -31,7 +31,7 @@ open Q
 type let_clause_kind =
   | LETTOPCLAUSE of Names.identifier * constr_expr
   | LETCLAUSE of
-      (Names.identifier Util.located * (constr_expr, Libnames.reference) may_eval option * raw_tactic_arg)
+      (Names.identifier Util.located * raw_tactic_expr option * raw_tactic_arg)
 
 ifdef Quotify then
 module Prelude = struct
@@ -82,7 +82,7 @@ GEXTEND Gram
       | id = base_ident; ":"; c = Constr.constr; ":="; "Proof" ->
           LETTOPCLAUSE (id, c)
       | id = identref; ":"; c = constrarg; ":="; te = tactic_letarg ->
-          LETCLAUSE (id, Some c, te)
+          LETCLAUSE (id, Some (TacArg(ConstrMayEval c)), te)
       |	id = base_ident; ":"; c = Constr.constr ->
 	  LETTOPCLAUSE (id, c) ] ]
   ;
@@ -150,35 +150,13 @@ GEXTEND Gram
 	  [IDENT "In" | "in"]; body = tactic_expr -> TacLetRecIn (rc::rcl,body)
       | IDENT "Let"; llc = LIST1 let_clause SEP "And"; IDENT "In";
           u = tactic_expr -> TacLetIn (make_letin_clause loc llc,u)
-(* Let cas LetCut est subsumé par "Assert id := c" tandis que le cas
-   StartProof ne fait pas vraiment de sens en tant que sous-expression
-   d'une tactique complexe... 
-      |	IDENT "Let"; llc = LIST1 let_clause SEP "And" -> 
-        (match llc with
-	| [LETTOPCLAUSE (id,c)] ->
-	    VernacStartProof ((NeverDischarge,false),id,c,true,(fun _ _ -> ()))
-        | l ->
-	    let l = List.map (function
-	      | LETCLAUSE (id,Some a,t) -> (id,a,t)
-	      | _ -> user_err_loc (loc, "", str "Syntax Error")) l in
-	    TacLetCut (loc, l))
-*)
-(*
-      |	IDENT "Let"; llc = LIST1 let_clause SEP "And";
-        tb = Vernac_.theorem_body; "Qed" ->
-          (match llc with
-	    | [LETTOPCLAUSE (id,c)] ->
-		EscapeVernac <:ast< (TheoremProof "LETTOP" $id $c $tb) >>
-	    | _ ->
-		errorlabstrm "Gram.tactic_atom" (str "Not a LETTOPCLAUSE"))
-*)
 
       | IDENT "Match"; IDENT "Context"; IDENT "With"; mrl = match_context_list
         -> TacMatchContext (false,mrl)
       | IDENT "Match"; IDENT "Reverse"; IDENT "Context"; IDENT "With"; mrl = match_context_list
         -> TacMatchContext (true,mrl)
       |	IDENT "Match"; c = constrarg; IDENT "With"; mrl = match_list ->
-        TacMatch (c,mrl)
+        TacMatch (TacArg(ConstrMayEval c),mrl)
 (*To do: put Abstract in Refiner*)
       | IDENT "Abstract"; tc = tactic_expr -> TacAbstract (tc,None)
       | IDENT "Abstract"; tc = tactic_expr; "using";  s = base_ident ->
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index 9d8dea149..5a1f13132 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -31,7 +31,7 @@ open Q
 type let_clause_kind =
   | LETTOPCLAUSE of Names.identifier * constr_expr
   | LETCLAUSE of
-      (Names.identifier Util.located * (constr_expr, Libnames.reference) may_eval option * raw_tactic_arg)
+      (Names.identifier Util.located * raw_tactic_expr option * raw_tactic_arg)
 
 ifdef Quotify then
 module Prelude = struct
@@ -99,7 +99,7 @@ GEXTEND Gram
       | "match"; IDENT "reverse"; IDENT "context"; "with";
         mrl = match_context_list; "end" ->
           TacMatchContext (true,mrl)
-      |	"match"; c = constrarg; "with"; mrl = match_list; "end" ->
+      |	"match"; c = tactic_expr; "with"; mrl = match_list; "end" ->
           TacMatch (c,mrl)
 (*To do: put Abstract in Refiner*)
       | IDENT "abstract"; tc = tactic_expr -> TacAbstract (tc,None)
@@ -116,7 +116,7 @@ GEXTEND Gram
       | st = simple_tactic -> TacAtom (loc,st)
       | IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
 	  TacArg(ConstrMayEval (ConstrEval (rtc,c)))
-      | IDENT "inst"; id = identref; "["; c = Constr.lconstr; "]" ->
+      | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" ->
 	  TacArg(ConstrMayEval (ConstrContext (id,c)))
       | IDENT "check"; c = Constr.constr ->
 	  TacArg(ConstrMayEval (ConstrTypeOf c))
@@ -148,11 +148,13 @@ GEXTEND Gram
   let_clause:
     [ [ id = identref; ":="; te = tactic_expr ->
           LETCLAUSE (id, None, arg_of_expr te)
-      | (_,id) = identref; ":"; c = Constr.constr; ":="; IDENT "proof" ->
+      | 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 = constrarg; ":="; te = tactic_expr ->
+      | id = identref; ":"; c = tactic_expr; ":="; te = tactic_expr ->
           LETCLAUSE (id, Some c, arg_of_expr te)
-      |	(_,id) = identref; ":"; c = Constr.lconstr ->
+      |	(_,id) = identref; ":"; c = Constr.constr ->
 	  LETTOPCLAUSE (id, c) ] ]
   ;
   rec_clause:
@@ -160,16 +162,16 @@ GEXTEND Gram
           (name,(it,body)) ] ]
   ;
   match_pattern:
-    [ [ id = Constr.lconstr_pattern; "["; pc = Constr.lconstr_pattern; "]" ->
-        let s = coerce_to_id id in Subterm (Some s, pc)
-      | "["; pc = Constr.lconstr_pattern; "]" -> Subterm (None,pc)
+    [ [ IDENT "context";  oid = OPT Constr.ident;
+          "["; pc = Constr.lconstr_pattern; "]" ->
+        Subterm (oid, pc)
       | pc = Constr.lconstr_pattern -> Term pc ] ]
   ;
   match_hyps:
     [ [ na = name; ":"; mp =  match_pattern -> Hyp (na, mp) ] ]
   ;
   match_context_rule:
-    [ [ "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; "]";
+    [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
         "=>"; te = tactic_expr -> Pat (largs, mp, te)
       | "_"; "=>"; te = tactic_expr -> All te ] ]
   ;
@@ -178,7 +180,7 @@ GEXTEND Gram
       | "|"; mrl = LIST1 match_context_rule SEP "|" -> mrl ] ]
   ;
   match_rule:
-    [ [ "["; mp = match_pattern; "]"; "=>"; te = tactic_expr -> Pat ([],mp,te)
+    [ [ mp = match_pattern; "=>"; te = tactic_expr -> Pat ([],mp,te)
       | "_"; "=>"; te = tactic_expr -> All te ] ]
   ;
   match_list:
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 0d7230453..968415de1 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -631,12 +631,8 @@ and pr6 = function
   | TacLetIn (llc,u) ->
       v 0
        (hv 0 (pr_let_clauses pr_tacarg0 llc ++ spc () ++ str "In") ++ fnl () ++ prtac u)
-  | TacLetCut llc ->
-      pr_let_clauses pr_tacarg0
-        (List.map (fun (id,c,t) -> ((dummy_loc,id),Some c,t)) llc)
-      ++ fnl ()
   | TacMatch (t,lrul) ->
-      hov 0 (str "Match" ++ spc () ++ pr_may_eval pr_constr pr_cst t ++ spc()
+      hov 0 (str "Match" ++ spc () ++ pr6 t ++ spc()
         ++ str "With"
         ++ prlist
 	  (fun r -> fnl () ++ str "|" ++ spc () ++
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 44e78462f..7dd14d87a 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -481,15 +481,12 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
       let f =
 	mlexpr_of_triple
 	  (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_ident)
-	  (mlexpr_of_option (mlexpr_of_may_eval mlexpr_of_constr))
+	  (mlexpr_of_option mlexpr_of_tactic)
 	  mlexpr_of_tactic_arg in
       <:expr< Tacexpr.TacLetIn $mlexpr_of_list f l$ $mlexpr_of_tactic t$ >>
-(*
-  | Tacexpr.TacLetCut of (identifier * t * tactic_expr) list
-*)
   | Tacexpr.TacMatch (t,l) ->
       <:expr< Tacexpr.TacMatch
-        $mlexpr_of_may_eval mlexpr_of_constr t$
+        $mlexpr_of_tactic t$
         $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>>
   | Tacexpr.TacMatchContext (lr,l) ->
       <:expr< Tacexpr.TacMatchContext