Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'ClearBody H' et 'Assert H := c'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2104 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 28 insertions, 4 deletions

diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml
index 57bb5d9753..b440546609 100644
--- a/tactics/tacentries.ml
+++ b/tactics/tacentries.ml
@@ -30,6 +30,7 @@ let v_left          = hide_tactic "Left"          dyn_left
 let v_right         = hide_tactic "Right"         dyn_right
 let v_split         = hide_tactic "Split"         dyn_split
 let v_clear         = hide_tactic "Clear"         dyn_clear
+let v_clear_body    = hide_tactic "ClearBody"     dyn_clear_body
 let v_move          = hide_tactic "Move"          dyn_move
 let v_move_dep      = hide_tactic "MoveDep"       dyn_move_dep
 let v_apply         = hide_tactic "Apply"         dyn_apply
@@ -37,6 +38,7 @@ let v_cutAndResolve = hide_tactic "CutAndApply"   dyn_cut_and_apply
 let v_cut           = hide_tactic "Cut"           dyn_cut
 let v_truecut       = hide_tactic "TrueCut"       dyn_true_cut
 let v_lettac        = hide_tactic "LetTac"        dyn_lettac
+let v_forward       = hide_tactic "Forward"       dyn_forward
 let v_generalize    = hide_tactic "Generalize"    dyn_generalize
 let v_generalize_dep = hide_tactic "GeneralizeDep" dyn_generalize_dep
 let v_specialize    = hide_tactic "Specialize"    dyn_new_hyp
diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli
index 70266c09f9..cb5cf8385e 100644
--- a/tactics/tacentries.mli
+++ b/tactics/tacentries.mli
@@ -31,6 +31,7 @@ val v_left          : tactic_arg list -> tactic
 val v_right         : tactic_arg list -> tactic
 val v_split         : tactic_arg list -> tactic
 val v_clear         : tactic_arg list -> tactic
+val v_clear_body    : tactic_arg list -> tactic
 val v_move          : tactic_arg list -> tactic
 val v_move_dep      : tactic_arg list -> tactic
 val v_apply         : tactic_arg list -> tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 11c37aa3bf..441cb2aad7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -103,6 +103,7 @@ let refine          = Tacmach.refine
 let convert_concl   = Tacmach.convert_concl
 let convert_hyp     = Tacmach.convert_hyp
 let thin            = Tacmach.thin 
+let thin_body       = Tacmach.thin_body 
 let move_hyp        = Tacmach.move_hyp 
 
 let mutual_fix   = Tacmach.mutual_fix
@@ -769,17 +770,19 @@ let letin_tac with_eq name c occs gl =
   let t = pf_type_of gl c in
   let tmpcl = List.fold_right mkNamedProd_or_LetIn depdecls ccl in
   let args = instance_from_named_context depdecls in
-  let newcl =
+  let newcl = mkNamedLetIn id c t tmpcl in
+(*
     if with_eq then
-      mkNamedLetIn id c t tmpcl
     else (* To fix : add c to args, or use LetIn and clear the body *)
-      mkNamedProd id t tmpcl
+      mkNamed id t tmpcl
   in
+*)
   let lastlhyp = if marks=[] then None else snd (List.hd marks) in
   tclTHENLIST
     [ apply_type newcl args;
       thin (List.map (fun (id,_,_) -> id) depdecls);
       intro_gen (IntroMustBe id) lastlhyp false;
+      if with_eq then tclIDTAC else thin_body [id];
       intros_move marks ] gl
 
 let check_hypotheses_occurrences_list env occl =
@@ -802,6 +805,13 @@ let dyn_lettac args gl = match args with
       letin_tac true (Name id) c (o,l) gl
   | l -> bad_tactic_args "letin" l
 
+let dyn_forward args gl = match args with
+  | [Command com; Identifier id] ->
+      letin_tac false (Name id) (pf_interp_constr gl com) (None,[]) gl
+  | [Constr c; Identifier id]    ->
+      letin_tac false (Name id) c (None,[]) gl
+  | l -> bad_tactic_args "forward" l
+
 (********************************************************************)
 (*               Exact tactics                                      *)
 (********************************************************************)
@@ -864,7 +874,14 @@ let dyn_clear = function
   | [Clause ids] ->
       let out = function InHyp id -> id | _ -> assert false in
       clear (List.map out ids)
-  | _ -> assert false
+  | l -> bad_tactic_args "clear" l
+
+let clear_body = thin_body
+let dyn_clear_body = function
+  | [Clause ids] ->
+      let out = function InHyp id -> id | _ -> assert false in
+      clear_body (List.map out ids)
+  | l -> bad_tactic_args "clear_body" l
 
 (* Clears a list of identifiers clauses form the context *)
 (*
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index a5244b7f85..8751fcb5cb 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -151,6 +151,9 @@ val clear         : identifier list -> tactic
 val clear_one     : identifier -> tactic
 val dyn_clear     : tactic_arg list -> tactic
 
+val clear_body    : identifier list -> tactic
+val dyn_clear_body : tactic_arg list -> tactic
+
 val clear_clauses : identifier list -> tactic
 val clear_clause  : identifier -> tactic
 
@@ -264,6 +267,7 @@ val cut_in_parallel             : constr list -> tactic
 val dyn_cut                     : tactic_arg list -> tactic
 val dyn_true_cut                : tactic_arg list -> tactic
 val dyn_lettac                  : tactic_arg list -> tactic
+val dyn_forward                 : tactic_arg list -> tactic
 
 val generalize                  : constr list -> tactic
 val dyn_generalize              : tactic_arg list -> tactic