Remplacement cut_intro par true_cut_anon

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

1 files changed, 13 insertions, 12 deletions

diff --git a/tactics/inv.ml b/tactics/inv.ml
index d5f42aa8d..68b2ca4ab 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -369,16 +369,17 @@ let res_case_then gene thin indbinding id status gl =
     if gene then case_trailer_gene thin neqns else case_trailer thin neqns
   in
   (tclTHENS
-     (cut_intro cut_concl)
-     [onLastHyp
+     (true_cut_anon cut_concl)
+     [case_tac (introCaseAssumsThen case_trailer_tac)
+        (Some elim_predicate) ([],[]) newc;
+      onLastHyp
         (fun id ->
-           (tclTHEN (applyUsing
-                       (applist(mkVar id,
-                                list_tabulate
-                                  (fun _ -> mkMeta(Clenv.new_meta())) neqns)))
-              Auto.default_auto));
-      case_tac (introCaseAssumsThen case_trailer_tac)
-        (Some elim_predicate) ([],[]) newc])
+           (tclTHEN
+              (applyUsing
+                 (applist(mkVar id,
+                          list_tabulate
+                            (fun _ -> mkMeta(Clenv.new_meta())) neqns)))
+              Auto.default_auto))])
   gl
 
 (* Error messages of the inversion tactics *)
@@ -410,10 +411,10 @@ let wrap_inv_error id = function
   | Not_found  ->  errorlabstrm "Inv" (not_found_message [id]) 
   | e -> raise e
 
-let inv gene com status id =
-  let inv_tac = res_case_then gene com [] id status in
+let inv gene thin status id =
+  let inv_tac = res_case_then gene thin [] id status in
   let tac =
-    if com = Some true (* if Inversion_clear, clear the hypothesis *) then 
+    if thin = Some true (* if Inversion_clear, clear the hypothesis *) then 
       tclTHEN inv_tac (tclTRY (clear_clause id))
     else 
       inv_tac