Removing redundant internal variants of apply tactic and simplification of ML names

(late consequences of commit r12603)

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

4 files changed, 34 insertions, 29 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index ad1ee8630a..c240d5f530 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,6 +2,21 @@
 = CHANGES BETWEEN COQ V8.2 AND COQ V8.3 =
 =========================================
 
+** Internal tactics renamed
+
+There is no more difference between bindings and ebindings. The
+following tactics are therefore renamed
+
+apply_with_ebindings_gen -> apply_with_bindings_gen
+left_with_ebindings -> left_with_bindings
+right_with_ebindings -> right_with_bindings
+split_with_ebindings -> split_with_bindings
+
+and the following tactics are removed
+
+apply_with_ebindings (use instead apply_with_bindings)
+eapply_with_ebindings (use instead eapply_with_bindings)
+
 ** Obsolete functions in typing.ml
 
 For mtype_of, msort_of, mcheck, now use type_of, sort_of, check
@@ -15,7 +30,6 @@ lookup_name_as_renamed -> lookup_name_as_displayed
 next_global_ident_away true -> next_ident_away_in_goal
 next_global_ident_away false -> next_global_ident_away
 
-
 ** Cleaning in commmand.ml
 
 Functions about starting/ending a lemma are in lemmas.ml
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 756212f0a7..4fed5d27cf 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -32,7 +32,7 @@ let h_vm_cast_no_check c =
   abstract_tactic (TacVmCastNoCheck c) (vm_cast_no_check c)
 let h_apply simple ev cb =
   abstract_tactic (TacApply (simple,ev,List.map snd cb,None))
-    (apply_with_ebindings_gen simple ev cb)
+    (apply_with_bindings_gen simple ev cb)
 let h_apply_in simple ev cb (id,ipat as inhyp) =
   abstract_tactic (TacApply (simple,ev,List.map snd cb,Some inhyp))
     (apply_in simple ev id cb ipat)
@@ -94,9 +94,9 @@ let h_rename l =
 let h_revert l = abstract_tactic (TacRevert l) (revert l)
 
 (* Constructors *)
-let h_left ev l  = abstract_tactic (TacLeft (ev,l)) (left_with_ebindings ev l)
-let h_right ev l = abstract_tactic (TacRight (ev,l)) (right_with_ebindings ev l)
-let h_split ev l = abstract_tactic (TacSplit (ev,false,l)) (split_with_ebindings ev l)
+let h_left ev l  = abstract_tactic (TacLeft (ev,l)) (left_with_bindings ev l)
+let h_right ev l = abstract_tactic (TacRight (ev,l)) (right_with_bindings ev l)
+let h_split ev l = abstract_tactic (TacSplit (ev,false,l)) (split_with_bindings ev l)
 (* Moved to tacinterp because of dependencies in Tacinterp.interp
 let h_any_constructor t =
   abstract_tactic (TacAnyConstructor t) (any_constructor t)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 120b3510bb..51aa86613e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -961,25 +961,19 @@ let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 =
   in
   try_main_apply with_destruct c gl0
 
-let rec apply_with_ebindings_gen b e = function
+let rec apply_with_bindings_gen b e = function
   | [] -> tclIDTAC
   | [cb] -> general_apply b b e cb
   | cb::cbl ->
-      tclTHENLAST (general_apply b b e cb) (apply_with_ebindings_gen b e cbl)
+      tclTHENLAST (general_apply b b e cb) (apply_with_bindings_gen b e cbl)
 
-let apply_with_ebindings cb =
-  apply_with_ebindings_gen false false [dloc,cb]
+let apply_with_bindings cb = apply_with_bindings_gen false false [dloc,cb]
 
-let eapply_with_ebindings cb =
-  apply_with_ebindings_gen false true [dloc,cb]
+let eapply_with_bindings cb = apply_with_bindings_gen false true [dloc,cb]
 
-let apply_with_bindings cb = apply_with_ebindings_gen false false [dloc,cb]
+let apply c = apply_with_bindings_gen false false [dloc,(c,NoBindings)]
 
-let eapply_with_bindings cb = apply_with_ebindings_gen false true [dloc,cb]
-
-let apply c = apply_with_ebindings_gen false false [dloc,(c,NoBindings)]
-
-let eapply c = apply_with_ebindings_gen false true [dloc,(c,NoBindings)]
+let eapply c = apply_with_bindings_gen false true [dloc,(c,NoBindings)]
 
 let apply_list = function
   | c::l -> apply_with_bindings (c,ImplicitBindings l)
@@ -1226,15 +1220,15 @@ let any_constructor with_evars tacopt gl =
       (fun i -> tclTHEN (constructor_tac with_evars None i NoBindings) t)
       (interval 1 nconstr)) gl
 
-let left_with_ebindings  with_evars = constructor_tac with_evars (Some 2) 1
-let right_with_ebindings with_evars = constructor_tac with_evars (Some 2) 2
-let split_with_ebindings with_evars l =
+let left_with_bindings  with_evars = constructor_tac with_evars (Some 2) 1
+let right_with_bindings with_evars = constructor_tac with_evars (Some 2) 2
+let split_with_bindings with_evars l =
   tclMAP (constructor_tac with_evars (Some 1) 1) l
 
-let left           = left_with_ebindings false
+let left           = left_with_bindings false
 let simplest_left  = left NoBindings
 
-let right          = right_with_ebindings false
+let right          = right_with_bindings false
 let simplest_right = right NoBindings
 
 let split          = constructor_tac false (Some 1) 1
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index e8b53c7045..0e552bd408 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -178,15 +178,12 @@ val bring_hyps : named_context -> tactic
 val apply                 : constr -> tactic
 val eapply                : constr -> tactic
 
-val apply_with_ebindings_gen :
+val apply_with_bindings_gen :
   advanced_flag -> evars_flag -> constr with_bindings located list -> tactic
 
 val apply_with_bindings   : constr with_bindings -> tactic
 val eapply_with_bindings  : constr with_bindings -> tactic
 
-val apply_with_ebindings  : constr with_bindings -> tactic
-val eapply_with_ebindings : constr with_bindings -> tactic
-
 val cut_and_apply         : constr -> tactic
 
 val apply_in :
@@ -327,9 +324,9 @@ val left                 : constr bindings -> tactic
 val right                : constr bindings -> tactic
 val split                : constr bindings -> tactic
 
-val left_with_ebindings  : evars_flag -> constr bindings -> tactic
-val right_with_ebindings : evars_flag -> constr bindings -> tactic
-val split_with_ebindings : evars_flag -> constr bindings list -> tactic
+val left_with_bindings  : evars_flag -> constr bindings -> tactic
+val right_with_bindings : evars_flag -> constr bindings -> tactic
+val split_with_bindings : evars_flag -> constr bindings list -> tactic
 
 val simplest_left        : tactic
 val simplest_right       : tactic