'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

11 files changed, 86 insertions, 81 deletions

diff --git a/CHANGES b/CHANGES
index ea236df8c0..4862cd1197 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,8 +1,19 @@
 Changes from V8.0
 =================
 
+Gallina
+
 - Added disjunctive patterns in match-with patterns
 
+Ltac
+
+- Semantics of "match t with" changed: if a clause returns a
+  tactic, it is now applied to the current goal. If it fails, the next
+  clause or next matching subterm is tried (i.e. it behaves as "match
+  goal with").
+- New modifier "lazy" for "match t with" and "match goal with" telling
+  to delay the evaluation of tactic expression.
+
 Changes from V8.0beta to V8.0
 =============================
 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 3028019636..c7ab085263 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -794,7 +794,8 @@ and xlate_tactic =
 		   xlate_tactic t)
    | TacProgress t -> CT_progress(xlate_tactic t)
    | TacOrelse(t1,t2) -> CT_orelse(xlate_tactic t1, xlate_tactic t2)
-   | TacMatch (exp, rules) ->
+   | TacMatch (true,_,_) -> failwith "TODO: lazy match"
+   | TacMatch (false, exp, rules) ->
         CT_match_tac(xlate_tactic exp,
                      match List.map 
                        (function 
@@ -810,11 +811,11 @@ and xlate_tactic =
                          | [] -> assert false
                          | fst::others ->
                              CT_match_tac_rules(fst, others))
-   | TacMatchContext (_,[]) -> failwith ""
-   | TacMatchContext (false,rule1::rules) ->
+   | TacMatchContext (_,_,[]) | TacMatchContext (true,_,_) -> failwith ""
+   | TacMatchContext (false,false,rule1::rules) ->
          CT_match_context(xlate_context_rule rule1,
                           List.map xlate_context_rule rules)
-   | TacMatchContext (true,rule1::rules) ->
+   | TacMatchContext (false,true,rule1::rules) ->
          CT_match_context_reverse(xlate_context_rule rule1,
                           List.map xlate_context_rule rules)
    | TacLetIn (l, t) ->
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$>>
 (*
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 86991d4a48..3e925d4609 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -20,6 +20,7 @@ open Pattern
 type 'a or_metaid = AI of 'a | MetaId of loc * string
 
 type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
+type lazy_flag = bool      (* true = lazy             false = eager *)
 
 type raw_red_flag =
   | FBeta
@@ -205,8 +206,8 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr =
 
   | TacLetRecIn of (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
   | TacLetIn of (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr option * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
-  | TacMatch of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list
-  | TacMatchContext of direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list
+  | TacMatch of lazy_flag * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list
+  | TacMatchContext of lazy_flag * direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list
   | TacFun of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast
   | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index c811e9db94..6f459b15ce 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -774,10 +774,10 @@ and intern_tactic_seq ist = function
       let (l1,l2) = ist.ltacvars in
       let ist' = { ist with ltacvars = ((extract_let_names l)@l1,l2) } in
       ist.ltacvars, TacLetIn (l,intern_tactic ist' u)
-  | TacMatchContext (lr,lmr) ->
-      ist.ltacvars, TacMatchContext(lr, intern_match_rule ist lmr)
-  | TacMatch (c,lmr) ->
-      ist.ltacvars, TacMatch (intern_tactic ist c,intern_match_rule ist lmr)
+  | TacMatchContext (lz,lr,lmr) ->
+      ist.ltacvars, TacMatchContext(lz,lr, intern_match_rule ist lmr)
+  | TacMatch (lz,c,lmr) ->
+      ist.ltacvars, TacMatch (lz,intern_tactic ist c,intern_match_rule ist lmr)
   | TacId _ as x -> ist.ltacvars, x
   | TacFail (n,x) -> ist.ltacvars, TacFail (intern_int_or_var ist n,x)
   | TacProgress tac -> ist.ltacvars, TacProgress (intern_tactic ist tac)
@@ -959,13 +959,9 @@ let rec read_match_rule evc env lfun = function
 exception Not_coherent_metas
 exception Eval_fail of string
 
-let is_failure = function
-  | FailError _ | Stdpp.Exc_located (_,FailError _) -> true
-  | _ -> false
-
 let is_match_catchable = function
   | PatternMatchingFailure | Eval_fail _ -> true
-  | e -> is_failure e or Logic.catchable_exception e
+  | e -> Logic.catchable_exception e
 
 (* Verifies if the matched list is coherent with respect to lcm *)
 let rec verify_metas_coherence gl lcm = function
@@ -1324,8 +1320,8 @@ let rec val_interp ist gl (tac:glob_tactic_expr) =
   | TacLetIn (l,u) ->
       let addlfun = interp_letin ist gl l in
       val_interp { ist with lfun=addlfun@ist.lfun } gl u
-  | TacMatchContext (lr,lmr) -> interp_match_context ist gl lr lmr 
-  | TacMatch (c,lmr) -> interp_match ist gl c lmr
+  | TacMatchContext (lz,lr,lmr) -> interp_match_context ist gl lz lr lmr 
+  | TacMatch (lz,c,lmr) -> interp_match ist gl lz c lmr
   | TacArg a -> interp_tacarg ist gl a
   (* Delayed evaluation *)
   | t -> VTactic (dummy_loc,eval_tactic ist t)
@@ -1338,11 +1334,8 @@ let rec val_interp ist gl (tac:glob_tactic_expr) =
 
 and eval_tactic ist = function
   | TacAtom (loc,t) -> fun gl -> catch_error loc (interp_atomic ist gl t) gl
-  | TacFun (it,body) -> assert false
-  | TacLetRecIn (lrc,u) -> assert false
-  | TacLetIn (l,u) -> assert false
-  | TacMatchContext _ -> assert false
-  | TacMatch (c,lmr) -> assert false
+  | TacFun _ | TacLetRecIn _ | TacLetIn _ -> assert false
+  | TacMatchContext _ | TacMatch _ -> assert false
   | TacId s -> tclIDTAC_MESSAGE s
   | TacFail (n,s) -> tclFAIL (interp_int_or_var ist n) s
   | TacProgress tac -> tclPROGRESS (interp_tactic ist tac)
@@ -1424,10 +1417,10 @@ and tactic_of_value vle g =
   | _ -> raise NotTactic
 
 (* Evaluation with FailError catching *)
-and eval_with_fail ist tac goal =
+and eval_with_fail ist is_lazy goal tac =
   try
     (match val_interp ist goal tac with
-    | VTactic (loc,tac) -> VRTactic (catch_error loc tac goal)
+    | VTactic (loc,tac) when not is_lazy -> VRTactic (catch_error loc tac goal)
     | a -> a)
   with
     | Stdpp.Exc_located (_,FailError (0,s)) | FailError (0,s) ->
@@ -1480,14 +1473,12 @@ and interp_letin ist gl = function
     in (id,VConstr (mkCast (csr,typ)))::(interp_letin ist gl tl)
 
 (* Interprets the Match Context expressions *)
-and interp_match_context ist g lr lmr =
+and interp_match_context ist g lz lr lmr =
   let rec apply_goal_sub ist env goal nocc (id,c) csr mt mhyps hyps =
     let (lgoal,ctxt) = match_subterm nocc c csr in
     let lctxt = give_context ctxt id in
-    try apply_hyps_context ist env goal mt lctxt lgoal mhyps hyps
-    with
-    | e when is_failure e -> raise e
-    | e when is_match_catchable e ->
+    try apply_hyps_context ist env lz goal mt lctxt lgoal mhyps hyps
+    with e when is_match_catchable e ->
       apply_goal_sub ist env goal (nocc + 1) (id,c) csr mt mhyps hyps in
   let rec apply_match_context ist env goal nrs lex lpt = 
     begin
@@ -1496,11 +1487,9 @@ and interp_match_context ist g lr lmr =
     | (All t)::tl ->
       begin
         db_mc_pattern_success ist.debug;
-        try eval_with_fail ist t goal
-        with
-        | e when is_failure e -> raise e
-        | e when is_match_catchable e ->
-            apply_match_context ist env goal (nrs+1) (List.tl lex) tl
+        try eval_with_fail ist lz goal t
+        with e when is_match_catchable e ->
+          apply_match_context ist env goal (nrs+1) (List.tl lex) tl
       end
     | (Pat (mhyps,mgoal,mt))::tl ->
       let hyps = make_hyps (pf_hyps goal) in
@@ -1512,19 +1501,16 @@ and interp_match_context ist g lr lmr =
         (try
            let lgoal = matches mg concl in
            db_matched_concl ist.debug (pf_env goal) concl;
-           apply_hyps_context ist env goal mt [] lgoal mhyps hyps
-        with 
-        | e when is_failure e -> raise e
-        | e when is_match_catchable e ->
-            (match e with
-              | PatternMatchingFailure -> db_matching_failure ist.debug
-              | Eval_fail s -> db_eval_failure ist.debug s
-              | _ -> db_logic_failure ist.debug e);
-            apply_match_context ist env goal (nrs+1) (List.tl lex) tl)
+           apply_hyps_context ist env lz goal mt [] lgoal mhyps hyps
+        with e when is_match_catchable e ->
+          (match e with
+            | PatternMatchingFailure -> db_matching_failure ist.debug
+            | Eval_fail s -> db_eval_failure ist.debug s
+            | _ -> db_logic_failure ist.debug e);
+          apply_match_context ist env goal (nrs+1) (List.tl lex) tl)
       |	Subterm (id,mg) ->
         (try apply_goal_sub ist env goal 0 (id,mg) concl mt mhyps hyps
         with
-        | e when is_failure e -> raise e
         | PatternMatchingFailure ->
            apply_match_context ist env goal (nrs+1) (List.tl lex) tl))
     | _ ->
@@ -1540,7 +1526,7 @@ and interp_match_context ist g lr lmr =
     (read_match_rule (project g) env (fst (constr_list ist env)) lmr)
 
 (* Tries to match the hypotheses in a Match Context *)
-and apply_hyps_context ist env goal mt lctxt lgmatch mhyps hyps =
+and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps =
   let rec apply_hyps_context_rec lfun lmatch lhyps_rest current = function
     | Hyp ((_,hypname),mhyp)::tl as mhyps ->
         let (lids,lm,hyp_match,next) =
@@ -1551,15 +1537,13 @@ and apply_hyps_context ist env goal mt lctxt lgmatch mhyps hyps =
             let nextlhyps = list_except hyp_match lhyps_rest in
             apply_hyps_context_rec (lfun@lids) (lmatch@lm) nextlhyps
 	      (nextlhyps,0) tl
-          with
-          | e when is_failure e -> raise e
-	  | e when is_match_catchable e -> 
+          with e when is_match_catchable e -> 
 	      apply_hyps_context_rec lfun lmatch lhyps_rest next mhyps
         end
     | [] ->
 	let lmatch = List.map (fun (id,c) -> (id,VConstr c)) lmatch in
         db_mc_pattern_success ist.debug;
-        eval_with_fail {ist with lfun=lmatch@lfun@ist.lfun} mt goal
+        eval_with_fail {ist with lfun=lmatch@lfun@ist.lfun} lz goal mt
   in
   apply_hyps_context_rec lctxt lgmatch hyps (hyps,0) mhyps
 
@@ -1616,25 +1600,24 @@ and interp_genarg ist goal x =
   | ExtraArgType s -> lookup_interp_genarg s ist goal x
 
 (* Interprets the Match expressions *)
-and interp_match ist g constr lmr =
+and interp_match ist g lz constr lmr =
   let rec apply_match_subterm ist nocc (id,c) csr mt =
     let (lm,ctxt) = match_subterm nocc c csr in
     let lctxt = give_context ctxt id in
     let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in
-    try val_interp {ist with lfun=lm@lctxt@ist.lfun} g mt
+    try eval_with_fail {ist with lfun=lm@lctxt@ist.lfun} lz g mt
     with e when is_match_catchable e ->
       apply_match_subterm ist (nocc + 1) (id,c) csr mt
   in
   let rec apply_match ist csr = function
     | (All t)::_ ->
-        (try val_interp ist g t
+        (try eval_with_fail ist lz g t
          with e when is_match_catchable e -> apply_match ist csr [])
     | (Pat ([],Term c,mt))::tl ->
         (try
 	  let lm = matches c csr in
 	  let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in
-          val_interp
-            { ist with lfun=lm@ist.lfun } g mt
+          eval_with_fail { ist with lfun=lm@ist.lfun } lz g mt
          with e when is_match_catchable e -> apply_match ist csr tl)
     | (Pat ([],Subterm (id,c),mt))::tl ->
         (try apply_match_subterm ist 0 (id,c) csr mt
@@ -2029,10 +2012,10 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
   | TacLetIn (l,u) ->
       let l = List.map (fun (n,c,b) -> (n,option_app (subst_tactic subst) c,subst_tacarg subst b)) l in
       TacLetIn (l,subst_tactic subst u)
-  | TacMatchContext (lr,lmr) ->
-      TacMatchContext(lr, subst_match_rule subst lmr)
-  | TacMatch (c,lmr) ->
-      TacMatch (subst_tactic subst c,subst_match_rule subst lmr)
+  | TacMatchContext (lz,lr,lmr) ->
+      TacMatchContext(lz,lr, subst_match_rule subst lmr)
+  | TacMatch (lz,c,lmr) ->
+      TacMatch (lz,subst_tactic subst c,subst_match_rule subst lmr)
   | TacId _ | TacFail _ as x -> x
   | TacProgress tac -> TacProgress (subst_tactic subst tac:glob_tactic_expr)
   | TacAbstract (tac,s) -> TacAbstract (subst_tactic subst tac,s)
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
index 0aca9a758b..f61999362f 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt.v
@@ -22,12 +22,12 @@ Ltac compute_POS :=
   match goal with
   |  |- context [(Zpos (xI ?X1))] =>
       match constr:X1 with
-      | context [1%positive] => fail
+      | context [1%positive] => fail 1
       | _ => rewrite (BinInt.Zpos_xI X1)
       end
   |  |- context [(Zpos (xO ?X1))] =>
       match constr:X1 with
-      | context [1%positive] => fail
+      | context [1%positive] => fail 1
       | _ => rewrite (BinInt.Zpos_xO X1)
       end
   end.
diff --git a/theories7/ZArith/Zsqrt.v b/theories7/ZArith/Zsqrt.v
index a1ea30415f..fca9b8145a 100644
--- a/theories7/ZArith/Zsqrt.v
+++ b/theories7/ZArith/Zsqrt.v
@@ -23,11 +23,11 @@ Tactic Definition compute_POS :=
   Match Context With
   | [|- [(POS (xI ?1))]] ->
     (Match ?1 With
-     | [[xH]] -> Fail
+     | [[xH]] -> Fail 1
      | _ -> Rewrite (POS_xI ?1))
   | [|- [(POS (xO ?1))]] ->
     (Match ?1 With
-     | [[xH]] -> Fail
+     | [[xH]] -> Fail 1
      | _ -> Rewrite (POS_xO ?1)).
 
 Inductive sqrt_data [n : Z] : Set :=
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index b6e0514541..7596dc2c33 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -279,6 +279,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 "context [" ++ pr_pat a ++ str "]"
@@ -704,16 +706,16 @@ let rec pr_tac env inherited tac =
        ++ str " in") ++
        fnl () ++ pr_tac env (llet,E) u),
       llet
-  | TacMatch (t,lrul) ->
-      hov 0 (str "match " ++ pr_tac env ltop t ++ str " with"
+  | TacMatch (lz,t,lrul) ->
+      hov 0 (pr_lazy lz ++ str "match " ++ pr_tac env ltop t ++ str " with"
         ++ prlist
 	  (fun r -> fnl () ++ str "| " ++
             pr_match_rule true (pr_tac env ltop) pr_pat r)
 	lrul
         ++ fnl() ++ str "end"),
       lmatch
-  | TacMatchContext (lr,lrul) ->
-      hov 0 (
+  | TacMatchContext (lz,lr,lrul) ->
+      hov 0 (pr_lazy lz ++ 
 	str (if lr then "match reverse goal with" else "match goal with")
 	++ prlist
 	  (fun r -> fnl () ++ str "| " ++