From d2562604fcea7ef0b0c5658af8fe21003ef3953e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 7 Mar 2005 21:39:55 +0000
Subject: Added 'clear - id' to clear all hypotheses except the ones dependent
 in the statement of id

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6806 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/pbp.ml   | 2 +-
 contrib/interface/xlate.ml | 5 +++--
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'contrib/interface')

diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index ef9f1280bc..5329556619 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -177,7 +177,7 @@ let make_pbp_atomic_tactic = function
       TacAtom
 	(zz, TacElim ((make_var hyp_name,ExplicitBindings bind),None))
   | PbpTryClear l -> 
-      TacTry (TacAtom (zz, TacClear (List.map (fun s -> AI (zz,s)) l)))
+      TacTry (TacAtom (zz, TacClear (false,List.map (fun s -> AI (zz,s)) l)))
   | PbpSplit -> TacAtom (zz, TacSplit (false,NoBindings));;
 
 let rec make_pbp_tactic = function
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 60688b625f..1bf8e85fd5 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1125,11 +1125,12 @@ and xlate_tac =
         CT_decompose_list(CT_id_ne_list(id',l'),xlate_formula c)
     | TacDecomposeAnd c -> CT_decompose_record (xlate_formula c)
     | TacDecomposeOr c -> CT_decompose_sum(xlate_formula c)
-    | TacClear [] ->
+    | TacClear (false,[]) ->
 	xlate_error "Clear expects a non empty list of identifiers"
-    | TacClear (id::idl) ->
+    | TacClear (false,id::idl) ->
        let idl' = List.map xlate_hyp idl in
        CT_clear (CT_id_ne_list (xlate_hyp id, idl'))
+    | TacClear (true,_) -> xlate_error "TODO: 'clear - idl' and 'clear'"
     | (*For translating tactics/Inv.v *)
       TacInversion (NonDepInversion (k,idl,l),quant_hyp) ->
 	CT_inversion(compute_INV_TYPE k, xlate_quantified_hypothesis quant_hyp,
-- 
cgit v1.2.3