'match term' now evaluates by default. Added 'lazy' keyword to delay the evaluation of tactics

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

4 files changed, 22 insertions, 15 deletions

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index c39e6f7fdf..8defe13c1e 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -125,11 +125,11 @@ GEXTEND Gram
           u = tactic_expr -> TacLetIn (make_letin_clause loc llc,u)
 
       | IDENT "Match"; IDENT "Context"; IDENT "With"; mrl = match_context_list
-        -> TacMatchContext (false,mrl)
+        -> TacMatchContext (false,false,mrl)
       | IDENT "Match"; IDENT "Reverse"; IDENT "Context"; IDENT "With"; mrl = match_context_list
-        -> TacMatchContext (true,mrl)
+        -> TacMatchContext (false,true,mrl)
       |	IDENT "Match"; c = constrarg; IDENT "With"; mrl = match_list ->
-        TacMatch (TacArg(ConstrMayEval c),mrl)
+        TacMatch (false,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 578ab250d3..e18769f5a3 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -72,13 +72,13 @@ 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 "goal"; "with"; mrl = match_context_list; "end" ->
-          TacMatchContext (false,mrl)
-      | "match"; IDENT "reverse"; IDENT "goal"; "with";
+      | b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
+          TacMatchContext (b,false,mrl)
+      | b = match_key; IDENT "reverse"; IDENT "goal"; "with";
         mrl = match_context_list; "end" ->
-          TacMatchContext (true,mrl)
-      |	"match"; c = tactic_expr; "with"; mrl = match_list; "end" ->
-          TacMatch (c,mrl)
+          TacMatchContext (b,true,mrl)
+      |	b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" ->
+          TacMatch (b,c,mrl)
       | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
 	  TacFirst l
       | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
@@ -122,6 +122,9 @@ GEXTEND Gram
       | r = reference -> Reference r
       | "()" -> TacVoid ] ]
   ;
+  match_key:
+    [ [ b = [ IDENT "lazy" -> true | -> false ]; "match" -> b ] ]
+  ;
   input_fun:
     [ [ "_" -> None 
       | l = base_ident -> Some l ] ]
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index e093954f8b..8c78e4fc70 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -186,6 +186,8 @@ let pr_induction_kind = function
   | FullInversion -> str "Inversion"
   | FullInversionClear -> str "Inversion_clear"
 
+let pr_lazy lz = if lz then str "lazy " else mt ()
+
 let pr_match_pattern pr_pat = function
   | Term a -> pr_pat a
   | Subterm (None,a) -> str "[" ++ pr_pat a ++ str "]"
@@ -676,15 +678,15 @@ and pr6 = function
   | TacLetIn (llc,u) ->
       v 0
        (hv 0 (pr_let_clauses pr_tacarg0 llc ++ spc () ++ str "In") ++ fnl () ++ prtac u)
-  | TacMatch (t,lrul) ->
-      hov 0 (str "Match" ++ spc () ++ pr6 t ++ spc()
+  | TacMatch (lz,t,lrul) ->
+      hov 0 (pr_lazy lz ++ str "Match" ++ spc () ++ pr6 t ++ spc()
         ++ str "With"
         ++ prlist
 	  (fun r -> fnl () ++ str "|" ++ spc () ++
             pr_match_rule true pr_pat prtac r)
 	lrul)
-  | TacMatchContext (lr,lrul) ->
-      hov 0 (
+  | TacMatchContext (lz,lr,lrul) ->
+      hov 0 (pr_lazy lz ++ 
 	str (if lr then "Match Reverse Context With" else "Match Context With")
 	++ prlist
 	  (fun r -> fnl () ++ str "|" ++ spc () ++
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 5a214cde7f..3ed0256ff8 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -507,12 +507,14 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
 	  (mlexpr_of_option mlexpr_of_tactic)
 	  mlexpr_of_tactic_arg in
       <:expr< Tacexpr.TacLetIn $mlexpr_of_list f l$ $mlexpr_of_tactic t$ >>
-  | Tacexpr.TacMatch (t,l) ->
+  | Tacexpr.TacMatch (lz,t,l) ->
       <:expr< Tacexpr.TacMatch
+        $mlexpr_of_bool lz$
         $mlexpr_of_tactic t$
         $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>>
-  | Tacexpr.TacMatchContext (lr,l) ->
+  | Tacexpr.TacMatchContext (lz,lr,l) ->
       <:expr< Tacexpr.TacMatchContext 
+        $mlexpr_of_bool lz$
         $mlexpr_of_bool lr$
         $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>>
 (*