(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(*i $Id$ i*)

(*i*)
open Names
open Term
open Environ
open Sign
open Tacmach
open Proof_type
open Reduction
open Evd
open Evar_refiner
open Clenv
open Redexpr
open Tacticals
open Libnames
open Genarg
open Tacexpr
open Nametab
open Rawterm
(*i*)

(* Main tactics. *)

(*s General functions. *)

val type_clenv_binding : goal sigma ->
  constr * constr -> constr bindings  -> constr

val string_of_inductive : constr -> string
val head_constr       : constr -> constr list
val head_constr_bound : constr -> constr list -> constr list
val is_quantified_hypothesis : identifier -> goal sigma -> bool

exception Bound

(*s Primitive tactics. *)

val introduction    : identifier -> tactic
val refine          : constr -> tactic
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
val fix             : identifier option -> int -> tactic
val mutual_cofix    : identifier -> (identifier * constr) list -> tactic
val cofix           : identifier option -> tactic

(*s Introduction tactics. *)

val fresh_id : identifier list -> identifier -> goal sigma -> identifier

val intro                : tactic
val introf               : tactic
val intro_force          : bool -> tactic
val intro_move           : identifier option -> identifier option -> tactic

val intro_replacing      : identifier -> tactic
val intro_using          : identifier -> tactic
val intro_mustbe_force   : identifier -> tactic
val intros_using         : identifier list -> tactic
val intro_erasing        : identifier -> tactic
val intros_replacing     : identifier list -> tactic

val intros               : tactic

(* [depth_of_quantified_hypothesis b h g] returns the index of [h] in
   the conclusion of goal [g], up to head-reduction if [b] is [true] *)
val depth_of_quantified_hypothesis :
  bool -> quantified_hypothesis -> goal sigma -> int

val intros_until_n_wored : int -> tactic
val intros_until         : quantified_hypothesis -> tactic

val intros_clearing      : bool list -> tactic

(* Assuming a tactic [tac] depending on an hypothesis identifier,
   [try_intros_until tac arg] first assumes that arg denotes a
   quantified hypothesis (denoted by name or by index) and try to
   introduce it in context before to apply [tac], otherwise assume the
   hypothesis is already in context and directly apply [tac] *)

val try_intros_until :
  (identifier -> tactic) -> quantified_hypothesis -> tactic

(*s Introduction tactics with eliminations. *)

val intro_pattern     : identifier option -> intro_pattern_expr      -> tactic
val intro_patterns    : intro_pattern_expr list -> tactic
val intros_pattern    : identifier option -> intro_pattern_expr list -> tactic

(*s Exact tactics. *)

val assumption       : tactic
val exact_no_check   : constr -> tactic
val exact_check      : constr -> tactic
val exact_proof      : Topconstr.constr_expr -> tactic

(*s Reduction tactics. *)

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_in_concl   : tactic_reduction * cast_kind -> tactic
val change_in_concl   : constr occurrences option -> constr -> tactic
val change_in_hyp     : constr occurrences option -> constr -> hyp_location ->
  tactic
val red_in_concl      : tactic
val red_in_hyp        : hyp_location        -> tactic
val red_option        : simple_clause -> tactic
val hnf_in_concl      : tactic
val hnf_in_hyp        : hyp_location        -> tactic
val hnf_option        : simple_clause -> tactic
val simpl_in_concl    : tactic
val simpl_in_hyp      : hyp_location        -> tactic
val simpl_option      : simple_clause -> tactic
val normalise_in_concl : tactic
val normalise_in_hyp  : hyp_location        -> tactic
val normalise_option  : simple_clause -> tactic
val normalise_vm_in_concl : tactic
val unfold_in_concl   : (int list * evaluable_global_reference) list -> tactic
val unfold_in_hyp     : 
  (int list * evaluable_global_reference) list -> hyp_location -> tactic
val unfold_option     : 
  (int list * evaluable_global_reference) list -> simple_clause
    -> tactic
val reduce            : red_expr -> clause -> tactic
val change            :
  constr occurrences option -> constr -> clause -> tactic

val unfold_constr     : global_reference -> tactic
val pattern_option  : (int list * constr) list -> simple_clause -> tactic

(*s Modification of the local context. *)

val clear         : identifier list -> tactic
val clear_body    : identifier list -> tactic
val keep          : identifier list -> tactic

val new_hyp       : int option -> constr with_bindings -> tactic

val move_hyp      : bool -> identifier -> identifier -> tactic
val rename_hyp    : identifier -> identifier -> tactic

(*s Resolution tactics. *)

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_bindings   : constr with_bindings -> tactic

val cut_and_apply         : constr -> tactic

(*s Elimination tactics. *)

val general_elim  :
  constr with_bindings -> constr with_bindings -> ?allow_K:bool -> tactic
val general_elim_in :
  identifier -> constr with_bindings -> constr with_bindings -> tactic

val default_elim  : constr with_bindings -> tactic
val simplest_elim : constr -> tactic
val elim          : constr with_bindings -> constr with_bindings option -> tactic
val simple_induct     : quantified_hypothesis * (bool ref * intro_pattern_expr list ref list) list ref -> tactic

val new_induct : constr induction_arg -> constr with_bindings option ->
  intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref
  -> tactic

(*s Case analysis tactics. *)

val general_case_analysis : constr with_bindings ->  tactic
val simplest_case         : constr -> tactic

val simple_destruct          : quantified_hypothesis -> tactic
val new_destruct : constr induction_arg -> constr with_bindings option ->
  intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref
  -> tactic

(*s Eliminations giving the type instead of the proof. *)

val case_type         : constr  -> tactic
val elim_type         : constr  -> tactic

(*s Some eliminations which are frequently used. *)

val impE : identifier -> tactic
val andE : identifier -> tactic
val orE  : identifier -> tactic
val dImp : clause -> tactic
val dAnd : clause -> tactic
val dorE : bool -> clause ->tactic


(*s Introduction tactics. *)

val constructor_tac            : int option -> int -> 
                                 constr bindings  -> tactic
val one_constructor            : int -> constr bindings  -> tactic
val any_constructor            : tactic option -> tactic
val left                       : constr bindings -> tactic
val simplest_left              : tactic
val right                      : constr bindings -> tactic
val simplest_right             : tactic
val split                      : constr bindings -> tactic
val simplest_split             : tactic

(*s Logical connective tactics. *)

val register_setoid_reflexivity : tactic -> unit
val reflexivity                 : tactic
val intros_reflexivity          : tactic

val register_setoid_symmetry : tactic -> unit
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                : constr -> tactic
val intros_transitivity         : constr -> tactic

val cut                         : constr -> tactic
val cut_intro                   : constr -> tactic
val cut_replacing               : 
  identifier -> constr -> (tactic -> tactic) -> tactic
val cut_in_parallel             : constr list -> tactic

val assert_tac                  : bool -> name -> constr -> tactic
val true_cut                    : name -> constr -> tactic
val letin_tac                   : bool -> name -> constr -> clause -> tactic
val forward                     : bool -> name -> constr -> tactic
val generalize                  : constr list -> tactic
val generalize_dep              : constr  -> tactic

val tclABSTRACT : identifier option -> tactic -> tactic

val admit_as_an_axiom : tactic