Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle tactique primitive Cut basé sur un Let non dépendant; amélioration efficacité ancien Cut

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

4 files changed, 23 insertions, 2 deletions

diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml
index 384341e663..57bb5d9753 100644
--- a/tactics/tacentries.ml
+++ b/tactics/tacentries.ml
@@ -35,6 +35,7 @@ let v_move_dep      = hide_tactic "MoveDep"       dyn_move_dep
 let v_apply         = hide_tactic "Apply"         dyn_apply
 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_generalize    = hide_tactic "Generalize"    dyn_generalize
 let v_generalize_dep = hide_tactic "GeneralizeDep" dyn_generalize_dep
diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli
index 6c73aa4719..8d8a664dd7 100644
--- a/tactics/tacentries.mli
+++ b/tactics/tacentries.mli
@@ -36,6 +36,7 @@ val v_move_dep      : tactic_arg list -> tactic
 val v_apply         : tactic_arg list -> tactic
 val v_cutAndResolve : tactic_arg list -> tactic
 val v_cut           : tactic_arg list -> tactic
+val v_truecut       : tactic_arg list -> tactic
 val v_lettac        : tactic_arg list -> tactic
 val v_generalize    : tactic_arg list -> tactic
 val v_generalize_dep : tactic_arg list -> tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 72cd0efbd3..bfe2788d22 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -97,6 +97,8 @@ let bad_tactic_args s l =
 
 let introduction    = Tacmach.introduction 
 let intro_replacing = Tacmach.intro_replacing 
+let internal_cut    = Tacmach.internal_cut
+let internal_cut_rev = Tacmach.internal_cut_rev
 let refine          = Tacmach.refine
 let convert_concl   = Tacmach.convert_concl
 let convert_hyp     = Tacmach.convert_hyp
@@ -586,11 +588,27 @@ let dyn_cut_and_apply = function
 (*     Cut tactics        *)
 (**************************)
 
+let true_cut c gl =
+  match kind_of_term (hnf_type_of gl c) with
+    | IsSort _ ->
+        let id=next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
+        internal_cut id c gl
+    | _  -> error "Not a proposition or a type"
+
+let dyn_true_cut = function
+  | [Command com] -> tactic_com_sort true_cut com
+  | [Constr  c]   -> true_cut c
+  | l             -> bad_tactic_args "true_cut" l
+
 let cut c gl =
   match kind_of_term (hnf_type_of gl c) with
     | IsSort _ ->
-	apply_type (mkProd (Anonymous, c, pf_concl gl)) 
-          [mkMeta (new_meta())] gl
+        let id=next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
+        let t = mkProd (Anonymous, c, pf_concl gl) in
+        tclTHENS
+          (internal_cut_rev id c)
+          [tclTHEN (apply_type t [mkVar id]) (thin [id]);
+           tclIDTAC] gl
     | _  -> error "Not a proposition or a type"
 
 let dyn_cut = function
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c31923ce7b..a5244b7f85 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -262,6 +262,7 @@ val cut_intro                   : constr -> tactic
 val cut_replacing               : identifier -> constr -> tactic
 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 generalize                  : constr list -> tactic