From 56ab825d3fbcd1d517027875245d1cafda68a6dc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 11 Oct 2004 11:39:18 +0000
Subject: '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
---
 translate/pptacticnew.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'translate')

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 "| " ++
-- 
cgit v1.2.3