Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 101 insertions, 93 deletions

diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index fb5c0efd..0e552bd4 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tactics.mli 11735 2009-01-02 17:22:31Z herbelin $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Util
@@ -27,20 +27,14 @@ open Genarg
 open Tacexpr
 open Nametab
 open Rawterm
+open Pattern
 open Termops
 (*i*)
 
-val inj_open : constr -> open_constr
-val inj_red_expr : red_expr -> (open_constr, evaluable_global_reference) red_expr_gen
-val inj_ebindings : constr bindings -> open_constr bindings
-
 (* Main tactics. *)
 
 (*s General functions. *)
 
-val type_clenv_binding : goal sigma ->
-  constr * constr -> open_constr bindings  -> constr
-
 val string_of_inductive : constr -> string
 val head_constr       : constr -> constr * constr list
 val head_constr_bound : constr -> constr * constr list
@@ -56,19 +50,19 @@ val convert_concl   : constr -> cast_kind -> tactic
 val convert_hyp     : named_declaration -> tactic
 val thin            : identifier list -> tactic
 val mutual_fix      :
-  identifier -> int -> (identifier * int * constr) list -> tactic
+  identifier -> int -> (identifier * int * constr) list -> int -> tactic
 val fix             : identifier option -> int -> tactic
-val mutual_cofix    : identifier -> (identifier * constr) list -> tactic
+val mutual_cofix    : identifier -> (identifier * constr) list -> int -> tactic
 val cofix           : identifier option -> tactic
 
 (*s Introduction tactics. *)
 
+val fresh_id_in_env : identifier list -> identifier -> env -> identifier
 val fresh_id : identifier list -> identifier -> goal sigma -> identifier
 val find_intro_names : rel_context -> goal sigma -> identifier list
 
 val intro                : tactic
 val introf               : tactic
-val intro_force          : bool -> tactic
 val intro_move        : identifier option -> identifier move_location -> tactic
 
   (* [intro_avoiding idl] acts as intro but prevents the new identifier
@@ -106,9 +100,9 @@ val try_intros_until :
 (* Apply a tactic on a quantified hypothesis, an hypothesis in context
    or a term with bindings *)
 
-val onInductionArg : 
-  (constr with_ebindings -> tactic) ->
-    constr with_ebindings induction_arg -> tactic
+val onInductionArg :
+  (constr with_bindings -> tactic) ->
+    constr with_bindings induction_arg -> tactic
 
 (*s Introduction tactics with eliminations. *)
 
@@ -130,35 +124,35 @@ val exact_proof      : Topconstr.constr_expr -> tactic
 type tactic_reduction = env -> evar_map -> constr -> constr
 
 val reduct_in_hyp     : tactic_reduction -> hyp_location -> tactic
-val reduct_option     : tactic_reduction * cast_kind -> simple_clause -> tactic
+val reduct_option     : tactic_reduction * cast_kind -> goal_location -> tactic
 val reduct_in_concl   : tactic_reduction * cast_kind -> tactic
-val change_in_concl   : (occurrences * constr) option -> constr -> tactic
-val change_in_hyp     : (occurrences * constr) option -> constr -> 
+val change_in_concl   : (occurrences * constr_pattern) option -> constr -> 
+                        tactic
+val change_in_hyp     : (occurrences * constr_pattern) option -> constr ->
                         hyp_location -> tactic
 val red_in_concl      : tactic
-val red_in_hyp        : hyp_location        -> tactic
-val red_option        : simple_clause -> tactic
+val red_in_hyp        : hyp_location -> tactic
+val red_option        : goal_location -> tactic
 val hnf_in_concl      : tactic
-val hnf_in_hyp        : hyp_location        -> tactic
-val hnf_option        : simple_clause -> tactic
+val hnf_in_hyp        : hyp_location -> tactic
+val hnf_option        : goal_location -> tactic
 val simpl_in_concl    : tactic
-val simpl_in_hyp      : hyp_location        -> tactic
-val simpl_option      : simple_clause -> tactic
+val simpl_in_hyp      : hyp_location -> tactic
+val simpl_option      : goal_location -> tactic
 val normalise_in_concl : tactic
-val normalise_in_hyp  : hyp_location        -> tactic
-val normalise_option  : simple_clause -> tactic
+val normalise_in_hyp  : hyp_location -> tactic
+val normalise_option  : goal_location -> tactic
 val normalise_vm_in_concl : tactic
 val unfold_in_concl   :
   (occurrences * evaluable_global_reference) list -> tactic
-val unfold_in_hyp     : 
+val unfold_in_hyp     :
   (occurrences * evaluable_global_reference) list -> hyp_location -> tactic
-val unfold_option     : 
-  (occurrences * evaluable_global_reference) list -> simple_clause
-    -> tactic
+val unfold_option     :
+  (occurrences * evaluable_global_reference) list -> goal_location -> tactic
 val change            :
-  (occurrences * constr) option -> constr -> clause -> tactic
-val pattern_option    : 
-  (occurrences * constr) list -> simple_clause -> tactic
+  constr_pattern option -> constr -> clause -> tactic
+val pattern_option    :
+  (occurrences * constr) list -> goal_location -> tactic
 val reduce            : red_expr -> clause -> tactic
 val unfold_constr     : global_reference -> tactic
 
@@ -168,7 +162,7 @@ val clear         : identifier list -> tactic
 val clear_body    : identifier list -> tactic
 val keep          : identifier list -> tactic
 
-val specialize    : int option -> constr with_ebindings -> tactic
+val specialize    : int option -> constr with_bindings -> tactic
 
 val move_hyp      : bool -> identifier -> identifier move_location -> tactic
 val rename_hyp    : (identifier * identifier) list -> tactic
@@ -181,32 +175,30 @@ val apply_type : constr -> constr list -> tactic
 val apply_term : constr -> constr list -> tactic
 val bring_hyps : named_context -> tactic
 
-val apply                 : constr      -> tactic
-val apply_without_reduce  : constr      -> tactic
-val apply_list            : constr list -> tactic
-  
-val apply_with_ebindings_gen : 
-  advanced_flag -> evars_flag -> open_constr with_ebindings list -> tactic
+val apply                 : constr -> tactic
+val eapply                : constr -> tactic
+
+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  : open_constr with_ebindings -> tactic
-val eapply_with_ebindings : open_constr with_ebindings -> tactic
-
 val cut_and_apply         : constr -> tactic
 
-val apply_in : 
+val apply_in :
   advanced_flag -> evars_flag -> identifier -> 
-  open_constr with_ebindings list ->
-  intro_pattern_expr located option -> tactic
+    constr with_bindings located list ->
+    intro_pattern_expr located option -> tactic
+
+val simple_apply_in : identifier -> constr -> tactic
 
 (*s Elimination tactics. *)
 
 
 (*
    The general form of an induction principle is the following:
-   
+
    forall prm1 prm2 ... prmp,                          (induction parameters)
    forall Q1...,(Qi:Ti_1 -> Ti_2 ->...-> Ti_ni),...Qq, (predicates)
    branch1, branch2, ... , branchr,                    (branches of the principle)
@@ -229,66 +221,82 @@ val apply_in :
 
 (* [rel_contexts] and [rel_declaration] actually contain triples, and
    lists are actually in reverse order to fit [compose_prod]. *)
-type elim_scheme = { 
-  elimc: constr with_ebindings option;
+type elim_scheme = {
+  elimc: constr with_bindings option;
   elimt: types;
   indref: global_reference option;
+  index: int;              (* index of the elimination type in the scheme *)
   params: rel_context;     (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
   nparams: int;            (* number of parameters *)
   predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
   npredicates: int;        (* Number of predicates *)
   branches: rel_context;   (* branchr,...,branch1 *)
-  nbranches: int;          (* Number of branches *) 
+  nbranches: int;          (* Number of branches *)
   args: rel_context;       (* (xni, Ti_ni) ... (x1, Ti_1) *)
   nargs: int;              (* number of arguments *)
-  indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni) 
+  indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni)
 				     if HI is in premisses, None otherwise *)
-  concl: types;            (* Qi x1...xni HI (f...), HI and (f...) 
+  concl: types;            (* Qi x1...xni HI (f...), HI and (f...)
 			      are optional and mutually exclusive *)
   indarg_in_concl: bool;   (* true if HI appears at the end of conclusion *)
   farg_in_concl: bool;     (* true if (f...) appears at the end of conclusion *)
 }
 
 
-val compute_elim_sig : ?elimc: constr with_ebindings -> types -> elim_scheme
+val compute_elim_sig : ?elimc: constr with_bindings -> types -> elim_scheme
 val rebuild_elimtype_from_scheme: elim_scheme -> types
 
+(* elim principle with the index of its inductive arg *)
+type eliminator = {
+  elimindex : int option;  (* None = find it automatically *)
+  elimbody : constr with_bindings
+}
+
+val elimination_clause_scheme : evars_flag ->
+  bool -> int -> clausenv -> clausenv -> tactic
+
+val elimination_in_clause_scheme : evars_flag -> identifier -> int ->
+  clausenv -> clausenv -> tactic
+
+val general_elim_clause_gen : (int -> Clenv.clausenv -> 'a -> tactic) ->
+  'a -> eliminator -> tactic
+
 val general_elim  : evars_flag ->
-  constr with_ebindings -> constr with_ebindings -> ?allow_K:bool -> tactic
-val general_elim_in : evars_flag -> 
-  identifier -> constr with_ebindings -> constr with_ebindings -> tactic
+  constr with_bindings -> eliminator -> ?allow_K:bool -> tactic
+val general_elim_in : evars_flag ->
+  identifier -> constr with_bindings -> eliminator -> tactic
 
-val default_elim  : evars_flag -> constr with_ebindings -> tactic
+val default_elim  : evars_flag -> constr with_bindings -> tactic
 val simplest_elim : constr -> tactic
-val elim : 
-  evars_flag -> constr with_ebindings -> constr with_ebindings option -> tactic
+val elim :
+  evars_flag -> constr with_bindings -> constr with_bindings option -> tactic
 
 val simple_induct : quantified_hypothesis -> tactic
 
-val new_induct : evars_flag -> constr with_ebindings induction_arg list -> 
-  constr with_ebindings option -> 
-  intro_pattern_expr located option * intro_pattern_expr located option ->
-  clause option -> tactic
+val new_induct : evars_flag -> constr with_bindings induction_arg list ->
+  constr with_bindings option ->
+    intro_pattern_expr located option * intro_pattern_expr located option ->
+      clause option -> tactic
 
 (*s Case analysis tactics. *)
 
-val general_case_analysis : evars_flag -> constr with_ebindings ->  tactic
+val general_case_analysis : evars_flag -> constr with_bindings ->  tactic
 val simplest_case         : constr -> tactic
 
 val simple_destruct          : quantified_hypothesis -> tactic
-val new_destruct : evars_flag -> constr with_ebindings induction_arg list -> 
-  constr with_ebindings option -> 
-  intro_pattern_expr located option * intro_pattern_expr located option ->
-  clause option -> tactic
+val new_destruct : evars_flag -> constr with_bindings induction_arg list ->
+  constr with_bindings option ->
+    intro_pattern_expr located option * intro_pattern_expr located option ->
+      clause option -> tactic
 
 (*s Generic case analysis / induction tactics. *)
 
-val induction_destruct : evars_flag -> rec_flag -> 
-  (constr with_ebindings induction_arg list *
-   constr with_ebindings option *
-   (intro_pattern_expr located option * intro_pattern_expr located option) *
-   clause option) list ->
-    tactic
+val induction_destruct : rec_flag -> evars_flag ->
+  (constr with_bindings induction_arg list *
+  constr with_bindings option *
+  (intro_pattern_expr located option * intro_pattern_expr located option))
+  list *
+  clause option -> tactic
 
 (*s Eliminations giving the type instead of the proof. *)
 
@@ -307,18 +315,18 @@ val dorE : bool -> clause ->tactic
 
 (*s Introduction tactics. *)
 
-val constructor_tac      : evars_flag -> int option -> int -> 
-                           open_constr bindings  -> tactic
+val constructor_tac      : evars_flag -> int option -> int ->
+  constr bindings -> tactic
 val any_constructor      : evars_flag -> tactic option -> tactic
-val one_constructor      : int -> open_constr bindings  -> tactic
+val one_constructor      : int -> constr bindings  -> tactic
 
 val left                 : constr bindings -> tactic
 val right                : constr bindings -> tactic
 val split                : constr bindings -> tactic
 
-val left_with_ebindings  : evars_flag -> open_constr bindings -> tactic
-val right_with_ebindings : evars_flag -> open_constr bindings -> tactic
-val split_with_ebindings : evars_flag -> open_constr bindings -> 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
@@ -327,31 +335,32 @@ val simplest_split       : tactic
 (*s Logical connective tactics. *)
 
 val register_setoid_reflexivity : tactic -> unit
-val reflexivity_red             : bool -> goal sigma -> tactic option
+val reflexivity_red             : bool -> tactic
 val reflexivity                 : tactic
 val intros_reflexivity          : tactic
 
 val register_setoid_symmetry : tactic -> unit
-val symmetry_red                : bool -> goal sigma -> tactic option
+val symmetry_red                : bool -> tactic
 val symmetry                    : tactic
 val register_setoid_symmetry_in : (identifier -> tactic) -> unit
 val symmetry_in                 : identifier -> tactic
 val intros_symmetry             : clause -> tactic
 
-val register_setoid_transitivity : (constr -> tactic) -> unit
-val transitivity_red            : bool -> constr -> goal sigma -> tactic option
+val register_setoid_transitivity : (constr option -> tactic) -> unit
+val transitivity_red            : bool -> constr option -> tactic
 val transitivity                : constr -> tactic
-val intros_transitivity         : constr -> tactic
+val etransitivity               : tactic
+val intros_transitivity         : constr option -> tactic
 
 val cut                         : constr -> tactic
 val cut_intro                   : constr -> tactic
-val cut_replacing               : 
-  identifier -> constr -> (tactic -> tactic) -> tactic
+val assert_replacing            : identifier -> types -> tactic -> tactic
+val cut_replacing               : identifier -> types -> tactic -> tactic
 val cut_in_parallel             : constr list -> tactic
 
 val assert_as : bool -> intro_pattern_expr located option -> constr -> tactic
 val forward   : tactic option -> intro_pattern_expr located option -> constr -> tactic
-val letin_tac : (bool * intro_pattern_expr located) option -> name -> 
+val letin_tac : (bool * intro_pattern_expr located) option -> name ->
   constr -> types option -> clause -> tactic
 val assert_tac : name -> types -> tactic
 val assert_by  : name -> types -> tactic -> tactic
@@ -359,7 +368,7 @@ val pose_proof : name -> constr -> tactic
 
 val generalize      : constr list -> tactic
 val generalize_gen  : ((occurrences * constr) * name) list -> tactic
-val generalize_dep  : constr  -> tactic
+val generalize_dep  : ?with_let:bool (* Don't lose let bindings *) -> constr  -> tactic
 
 val unify           : ?state:Names.transparent_state -> constr -> constr -> tactic
 val resolve_classes : tactic
@@ -368,9 +377,8 @@ val tclABSTRACT : identifier option -> tactic -> tactic
 
 val admit_as_an_axiom : tactic
 
-val abstract_generalize : identifier -> ?generalize_vars:bool -> tactic
-
-val dependent_pattern : constr -> tactic
+val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> identifier -> tactic
+val specialize_eqs : identifier -> tactic
 
-val register_general_multi_rewrite : 
-  (bool -> evars_flag -> open_constr with_bindings -> clause -> tactic) -> unit
+val register_general_multi_rewrite :
+  (bool -> evars_flag -> constr with_bindings -> clause -> tactic) -> unit