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

5 files changed, 22 insertions, 5 deletions

diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index a33d648ed2..d5da2c86b9 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -66,7 +66,8 @@ let h_specialize n d = abstract_tactic (TacSpecialize (n,d)) (new_hyp n d)
 let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c)
 
 (* Context management *)
-let h_clear l = abstract_tactic (TacClear l) (clear l)
+let h_clear b l = abstract_tactic (TacClear (b,l))
+  ((if b then keep else clear) l)
 let h_clear_body l = abstract_tactic (TacClearBody l) (clear_body l)
 let h_move dep id1 id2 =
   abstract_tactic (TacMove (dep,id1,id2)) (move_hyp dep id1 id2)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index dc547c2a85..847d0caa75 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -73,7 +73,7 @@ val h_lapply          : constr -> tactic
 
 
 (* Context management *)
-val h_clear           : identifier list -> tactic
+val h_clear           : bool -> identifier list -> tactic
 val h_clear_body      : identifier list -> tactic
 val h_move            : bool -> identifier -> identifier -> tactic
 val h_rename          : identifier -> identifier -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index bd9c44def5..4ce3fcc04a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -726,7 +726,7 @@ let rec intern_atomic lf ist x =
   | TacLApply c -> TacLApply (intern_constr ist c)
 
   (* Context management *)
-  | TacClear l -> TacClear (List.map (intern_hyp_or_metaid ist) l)
+  | TacClear (b,l) -> TacClear (b,List.map (intern_hyp_or_metaid ist) l)
   | TacClearBody l -> TacClearBody (List.map (intern_hyp_or_metaid ist) l)
   | TacMove (dep,id1,id2) ->
     TacMove (dep,intern_hyp_or_metaid ist id1,intern_hyp_or_metaid ist id2)
@@ -1755,7 +1755,7 @@ and interp_atomic ist gl = function
   | TacLApply c -> h_lapply (pf_interp_constr ist gl c)
 
   (* Context management *)
-  | TacClear l -> h_clear (List.map (interp_hyp ist gl) l)
+  | TacClear (b,l) -> h_clear b (List.map (interp_hyp ist gl) l)
   | TacClearBody l -> h_clear_body (List.map (interp_hyp ist gl) l)
   | TacMove (dep,id1,id2) ->
       h_move dep (interp_hyp ist gl id1) (interp_hyp ist gl id2)
@@ -2004,7 +2004,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacLApply c -> TacLApply (subst_rawconstr subst c)
 
   (* Context management *)
-  | TacClear l as x -> x
+  | TacClear _ as x -> x
   | TacClearBody l as x -> x
   | TacMove (dep,id1,id2) as x -> x
   | TacRename (id1,id2) as x -> x
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7b595a0733..8835c16d2e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -840,6 +840,21 @@ let new_hyp mopt (c,lbind) g =
                (cut (pf_type_of g cut_pf)))
      ((tclORELSE (apply cut_pf) (exact_no_check cut_pf)))) g
 
+(* Keeping only a few hypotheses *)
+
+let keep hyps gl =
+  let env = Global.env() in
+  let ccl = pf_concl gl in
+  let cl,_ =
+    fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) ->
+      if List.mem hyp hyps
+	or List.exists (occur_var_in_decl env hyp) keep
+	or occur_var env hyp ccl
+      then (clear,decl::keep)
+      else (hyp::clear,keep))
+      ~init:([],[]) (pf_env gl)
+  in thin cl gl
+
 (************************)
 (* Introduction tactics *)
 (************************)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index b804de067d..34c4e6397b 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -144,6 +144,7 @@ val pattern_option  : (int list * constr) list -> simple_clause -> tactic
 
 val clear         : identifier list -> tactic
 val clear_body    : identifier list -> tactic
+val keep          : identifier list -> tactic
 
 val new_hyp       : int option -> constr with_bindings -> tactic