diff options
| author | herbelin | 2004-10-11 11:39:18 +0000 |
|---|---|---|
| committer | herbelin | 2004-10-11 11:39:18 +0000 |
| commit | 56ab825d3fbcd1d517027875245d1cafda68a6dc (patch) | |
| tree | d10d1b2e924a332f2d8ecfdffb2684e3908bce53 /translate | |
| parent | a807069e370eb1a8f4d7f4e8b72449017a68d891 (diff) | |
'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
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/pptacticnew.ml | 10 |
1 files changed, 6 insertions, 4 deletions
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 "| " ++ |