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

14 files changed, 40 insertions, 17 deletions

diff --git a/CHANGES b/CHANGES
index 8104f54eb5..25eb039ff1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -23,6 +23,7 @@ Ltac
 
 Tactics
 
+- Added "clear - id" to clear all hypotheses except the ones depending in id.
 - Added "dependent rewrite term" and "dependent rewrite term in hyp" (doc TODO)
 - The argument of Declare Left Step and Declare Right Step is now a term
   (it used to be a reference) (doc TODO)
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,
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index c578c66b3c..8972b0a210 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -322,7 +322,8 @@ GEXTEND Gram
 	  TacDAuto (n, p)
 
       (* Context management *)
-      | IDENT "Clear"; l = LIST1 id_or_ltac_ref -> TacClear l
+      | IDENT "Clear"; "-"; l = LIST1 id_or_meta -> TacClear (true, l)
+      | IDENT "Clear"; l = LIST0 id_or_meta -> TacClear (l=[], l)
       | IDENT "ClearBody"; l = LIST1 id_or_ltac_ref -> TacClearBody l
       | IDENT "Move"; id1 = id_or_ltac_ref; IDENT "after"; 
 	  id2 = id_or_ltac_ref -> TacMove (true,id1,id2)
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 49dd4fa309..c41de337b0 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -359,7 +359,8 @@ GEXTEND Gram
 	  TacDAuto (n, p)
 
       (* Context management *)
-      | IDENT "clear"; l = LIST1 id_or_meta -> TacClear l
+      | IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacClear (true, l)
+      | IDENT "clear"; l = LIST0 id_or_meta -> TacClear (l=[], l)
       | IDENT "clearbody"; l = LIST1 id_or_meta -> TacClearBody l
       | IDENT "move"; id1 = id_or_meta; IDENT "after"; id2 = id_or_meta -> 
 	  TacMove (true,id1,id2)
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index c6718c8a9e..52d6eb2d78 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -547,8 +547,9 @@ and pr_atom1 = function
       hov 1 (str "Auto" ++ pr_opt int n ++ str "Decomp" ++ pr_opt int p)
 
   (* Context management *)
-  | TacClear l ->
-      hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc pr_ident l)
+  | TacClear (keep,l) ->
+      hov 1 (str "Clear" ++ spc () ++ (if keep then str "- " else mt ()) ++
+             prlist_with_sep spc pr_ident l)
   | TacClearBody l ->
       hov 1 (str "ClearBody" ++ spc () ++ prlist_with_sep spc pr_ident l)
   | TacMove (b,id1,id2) ->
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 37dcc22b19..a411d0ddde 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -423,9 +423,9 @@ let rec mlexpr_of_atomic_tactic = function
       <:expr< Tacexpr.TacNewDestruct $mlexpr_of_induction_arg c$ $cbo$ ($ids$,ref []) >>
 
   (* Context management *)
-  | Tacexpr.TacClear l ->
+  | Tacexpr.TacClear (b,l) ->
       let l = mlexpr_of_list (mlexpr_of_hyp) l in
-      <:expr< Tacexpr.TacClear $l$ >>
+      <:expr< Tacexpr.TacClear $mlexpr_of_bool b$ $l$ >>
   | Tacexpr.TacClearBody l ->
       let l = mlexpr_of_list (mlexpr_of_hyp) l in
       <:expr< Tacexpr.TacClearBody $l$ >>
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index aab052d7b8..3d060a8a3f 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -156,7 +156,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacDAuto of int option * int option
 
   (* Context management *)
-  | TacClear of 'id list
+  | TacClear of bool * 'id list
   | TacClearBody of 'id list
   | TacMove of bool * 'id * 'id
   | TacRename of 'id * 'id
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
 
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index bb83d10309..29203afd0b 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -610,8 +610,9 @@ and pr_atom1 env = function
       hov 1 (str "auto" ++ pr_opt int n ++ str "decomp" ++ pr_opt int p)
 
   (* Context management *)
-  | TacClear l ->
-      hov 1 (str "clear" ++ spc () ++ prlist_with_sep spc pr_ident l)
+  | TacClear (keep,l) ->
+      hov 1 (str "clear" ++ spc () ++ (if keep then str "- " else mt ()) ++
+             prlist_with_sep spc pr_ident l)
   | TacClearBody l ->
       hov 1 (str "clearbody" ++ spc () ++ prlist_with_sep spc pr_ident l)
   | TacMove (b,id1,id2) ->