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
---
 contrib/interface/xlate.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'contrib/interface')

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