Renaming new_induct -> induction; new_destruct -> destruct.

5 files changed, 23 insertions, 21 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 2164830a7..8a2b13ebe 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -75,6 +75,8 @@
       check_evars_are_solved explicitly to check that evars are solved.
   See also the corresponding commit log.
 
+- Tactics API: new_induct -> induction; new_destruct -> destruct
+
 =========================================
 = CHANGES BETWEEN COQ V8.3 AND COQ V8.4 =
 =========================================
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 3f728ddcd..70a892a3b 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -26,8 +26,8 @@ let is_rec_info scheme_info =
 
 let choose_dest_or_ind scheme_info =
     if is_rec_info scheme_info
-    then Tactics.new_induct false
-    else Tactics.new_destruct false
+    then Tactics.induction false
+    else Tactics.destruct false
 
 let functional_induction with_clean c princl pat =
   Dumpglob.pause ();
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4175077d4..c3331a372 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3366,7 +3366,7 @@ let clear_unselected_context id inhyps cls gl =
 	  thin ids gl
       | None -> tclIDTAC gl
 
-let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
+let induction_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
   let inhyps = match cls with
   | Some {onhyps=Some hyps} -> List.map (fun ((_,id),_) -> id) hyps
   | _ -> [] in
@@ -3404,8 +3404,8 @@ let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
    atomic (using letins), then do induction. The specificity here is
    that all arguments and parameters of the scheme are given
    (mandatory for the moment), so we don't need to deal with
-    parameters of the inductive type as in new_induct_gen. *)
-let new_induct_gen_l isrec with_evars elim (eqname,names) lc =
+    parameters of the inductive type as in induction_gen. *)
+let induction_gen_l isrec with_evars elim (eqname,names) lc =
   if not (Option.is_empty eqname) then
     errorlabstrm "" (str "Do not know what to do with " ++
       Miscprint.pr_intro_pattern (Option.get eqname));
@@ -3451,14 +3451,14 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc =
    principles).
    TODO: really unify induction with one and induction with several
    args *)
-let induct_destruct isrec with_evars (lc,elim,names,cls) =
+let induction_destruct_core isrec with_evars (lc,elim,names,cls) =
   assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *)
   Proofview.Goal.raw_enter begin fun gl ->
   let ifi = is_functional_induction elim gl in
   if Int.equal (List.length lc) 1 && not ifi then
     (* standard induction *)
     onOpenInductionArg
-      (fun c -> new_induct_gen isrec with_evars elim names c cls)
+      (fun c -> induction_gen isrec with_evars elim names c cls)
       (List.hd lc)
   else begin
     (* functional induction *)
@@ -3481,7 +3481,7 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) =
 	(fun (c,lbind) ->
 	  if lbind != NoBindings then
 	    error "'with' clause not supported here.";
-	  new_induct_gen_l isrec with_evars elim names [c]) (List.hd lc)
+	  induction_gen_l isrec with_evars elim names [c]) (List.hd lc)
     | _ ->
       let newlc =
 	List.map (fun x ->
@@ -3489,28 +3489,28 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) =
 	  | ElimOnConstr (x,NoBindings) -> x
 	  | _ -> error "Don't know where to find some argument.")
 	  lc in
-      new_induct_gen_l isrec with_evars elim names newlc
+      induction_gen_l isrec with_evars elim names newlc
     end
   end
   end
 
 let induction_destruct isrec with_evars = function
   | [],_,_ -> Proofview.tclUNIT ()
-  | [a,b],el,cl -> induct_destruct isrec with_evars ([a],el,b,cl)
+  | [a,b],el,cl -> induction_destruct_core isrec with_evars ([a],el,b,cl)
   | (a,b)::l,None,cl ->
       Tacticals.New.tclTHEN
-        (induct_destruct isrec with_evars ([a],None,b,cl))
-        (Tacticals.New.tclMAP (fun (a,b) -> induct_destruct false with_evars ([a],None,b,cl)) l)
+        (induction_destruct_core isrec with_evars ([a],None,b,cl))
+        (Tacticals.New.tclMAP (fun (a,b) -> induction_destruct_core false with_evars ([a],None,b,cl)) l)
   | l,Some el,cl ->
       let check_basic_using = function
         | a,(None,None) -> a
 	| _ -> error "Unsupported syntax for \"using\"."
       in
       let l' = List.map check_basic_using l in
-      induct_destruct isrec with_evars (l', Some el, (None,None), cl)
+      induction_destruct_core isrec with_evars (l', Some el, (None,None), cl)
 
-let new_induct ev lc e idl cls = induct_destruct true ev (lc,e,idl,cls)
-let new_destruct ev lc e idl cls = induct_destruct false ev (lc,e,idl,cls)
+let induction ev lc e idl cls = induction_destruct_core true ev (lc,e,idl,cls)
+let destruct ev lc e idl cls = induction_destruct_core false ev (lc,e,idl,cls)
 
 (* The registered tactic, which calls the default elimination
  * if no elimination constant is provided. *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c48ef4451..0ee307c23 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -266,7 +266,7 @@ val elim :
 
 val simple_induct : quantified_hypothesis -> unit Proofview.tactic
 
-val new_induct : evars_flag -> 
+val induction : evars_flag -> 
   (evar_map * constr with_bindings) induction_arg list ->
   constr with_bindings option ->
     intro_pattern_expr located option * intro_pattern_expr located option ->
@@ -278,7 +278,7 @@ val general_case_analysis : evars_flag -> constr with_bindings ->  unit Proofvie
 val simplest_case         : constr -> unit Proofview.tactic
 
 val simple_destruct          : quantified_hypothesis -> unit Proofview.tactic
-val new_destruct : evars_flag ->
+val destruct : evars_flag ->
   (evar_map * constr with_bindings) induction_arg list ->
   constr with_bindings option ->
     intro_pattern_expr located option * intro_pattern_expr located option ->
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 5129beeab..de0459089 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -78,12 +78,12 @@ let sumbool = Coqlib.build_coq_sumbool
 let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb
 
 let induct_on c =
-  new_induct false
+  induction false
     [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
     None (None,None) None
 
 let destruct_on_using c id =
-  new_destruct false
+  destruct false
     [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
     None
     (None,Some (dl,IntroOrAndPattern [
@@ -92,7 +92,7 @@ let destruct_on_using c id =
     None
 
 let destruct_on c =
-  new_destruct false
+  destruct false
     [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
     None (None,None) None
 
@@ -592,7 +592,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                          apply_in false false freshz [Loc.ghost, (andb_prop(), NoBindings)] None;
                          Proofview.Goal.enter begin fun gl ->
                            let fresht = fresh_id (Id.of_string "Z") gl in
-                            (new_destruct false [Tacexpr.ElimOnConstr
+                            (destruct false [Tacexpr.ElimOnConstr
                                       (Evd.empty,((mkVar freshz,NoBindings)))]
                                   None
                                   (None, Some (dl,IntroOrAndPattern [[