Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 30 insertions, 30 deletions

diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 9270411a..36b0830d 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: hiddentac.mli 12102 2009-04-24 10:48:11Z herbelin $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
@@ -37,30 +37,30 @@ val h_exact           : constr -> tactic
 val h_exact_no_check  : constr -> tactic
 val h_vm_cast_no_check  : constr -> tactic
 
-val h_apply           : advanced_flag -> evars_flag -> 
-  open_constr with_bindings list -> tactic
-val h_apply_in        : advanced_flag -> evars_flag -> 
-  open_constr with_bindings list -> 
+val h_apply           : advanced_flag -> evars_flag ->
+  constr with_bindings located list -> tactic
+val h_apply_in        : advanced_flag -> evars_flag ->
+  constr with_bindings located list ->
   identifier * intro_pattern_expr located option -> tactic
 
-val h_elim            : evars_flag -> constr with_ebindings ->
-                        constr with_ebindings option -> tactic
+val h_elim            : evars_flag -> constr with_bindings ->
+                        constr with_bindings option -> tactic
 val h_elim_type       : constr -> tactic
-val h_case            : evars_flag -> constr with_ebindings -> tactic
+val h_case            : evars_flag -> constr with_bindings -> tactic
 val h_case_type       : constr -> tactic
 
 val h_mutual_fix      : hidden_flag -> identifier -> int ->
                         (identifier * int * constr) list -> tactic
 val h_fix             : identifier option -> int -> tactic
-val h_mutual_cofix    : hidden_flag -> identifier -> 
+val h_mutual_cofix    : hidden_flag -> identifier ->
                         (identifier * constr) list -> tactic
 val h_cofix           : identifier option -> tactic
 
-val h_cut             : constr -> tactic 
-val h_generalize      : constr list -> tactic 
-val h_generalize_gen  : (constr with_occurrences * name) list -> tactic 
-val h_generalize_dep  : constr -> tactic 
-val h_let_tac         : letin_flag -> name -> constr -> 
+val h_cut             : constr -> tactic
+val h_generalize      : constr list -> tactic
+val h_generalize_gen  : (constr with_occurrences * name) list -> tactic
+val h_generalize_dep  : constr -> tactic
+val h_let_tac         : letin_flag -> name -> constr ->
                         Tacticals.clause -> tactic
 
 (* Derived basic tactics *)
@@ -68,20 +68,20 @@ val h_let_tac         : letin_flag -> name -> constr ->
 val h_simple_induction   : quantified_hypothesis -> tactic
 val h_simple_destruct    : quantified_hypothesis -> tactic
 val h_simple_induction_destruct : rec_flag -> quantified_hypothesis -> tactic
-val h_new_induction   : evars_flag -> 
-  constr with_ebindings induction_arg list -> constr with_ebindings option ->
+val h_new_induction   : evars_flag ->
+  constr with_bindings induction_arg list -> constr with_bindings option ->
   intro_pattern_expr located option * intro_pattern_expr located option ->
   Tacticals.clause option -> tactic
-val h_new_destruct    : evars_flag -> 
-  constr with_ebindings induction_arg list -> constr with_ebindings option -> 
+val h_new_destruct    : evars_flag ->
+  constr with_bindings induction_arg list -> constr with_bindings option ->
   intro_pattern_expr located option * intro_pattern_expr located option ->
   Tacticals.clause option -> tactic
 val h_induction_destruct : rec_flag -> evars_flag ->
-  (constr with_ebindings induction_arg list * constr with_ebindings option * 
-   (intro_pattern_expr located option * intro_pattern_expr located option) *
-   Tacticals.clause option) list -> tactic
+  (constr with_bindings induction_arg list * constr with_bindings option *
+   (intro_pattern_expr located option * intro_pattern_expr located option)) list
+    * Tacticals.clause option -> tactic
 
-val h_specialize      : int option -> constr with_ebindings -> tactic
+val h_specialize      : int option -> constr with_bindings -> tactic
 val h_lapply          : constr -> tactic
 
 (* Automation tactic : see Auto *)
@@ -95,10 +95,10 @@ val h_rename          : (identifier*identifier) list -> tactic
 val h_revert          : identifier list -> tactic
 
 (* Constructors *)
-val h_constructor     : evars_flag -> int -> open_constr bindings -> tactic
-val h_left            : evars_flag -> open_constr bindings -> tactic
-val h_right           : evars_flag -> open_constr bindings -> tactic
-val h_split           : evars_flag -> open_constr bindings -> tactic
+val h_constructor     : evars_flag -> int -> constr bindings -> tactic
+val h_left            : evars_flag -> constr bindings -> tactic
+val h_right           : evars_flag -> constr bindings -> tactic
+val h_split           : evars_flag -> constr bindings list -> tactic
 
 val h_one_constructor : int -> tactic
 val h_simplest_left   : tactic
@@ -108,15 +108,15 @@ val h_simplest_right  : tactic
 (* Conversion *)
 val h_reduce          : Redexpr.red_expr -> Tacticals.clause -> tactic
 val h_change          :
-  constr with_occurrences option -> constr -> Tacticals.clause -> tactic
+  Pattern.constr_pattern option -> constr -> Tacticals.clause -> tactic
 
 (* Equivalence relations *)
 val h_reflexivity     : tactic
 val h_symmetry        : Tacticals.clause -> tactic
-val h_transitivity    : constr -> tactic
+val h_transitivity    : constr option -> tactic
 
-val h_simplest_apply  : constr -> tactic 
-val h_simplest_eapply : constr -> tactic 
+val h_simplest_apply  : constr -> tactic
+val h_simplest_eapply : constr -> tactic
 val h_simplest_elim   : constr -> tactic
 val h_simplest_case   : constr -> tactic