diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 111 |
1 files changed, 58 insertions, 53 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 5ceade1f..f8f32b79 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tactics.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Util open Names open Term @@ -26,14 +23,14 @@ open Libnames open Genarg open Tacexpr open Nametab -open Rawterm +open Glob_term open Pattern open Termops -(*i*) +open Unification -(* Main tactics. *) +(** Main tactics. *) -(*s General functions. *) +(** {6 General functions. } *) val string_of_inductive : constr -> string val head_constr : constr -> constr * constr list @@ -42,7 +39,7 @@ val is_quantified_hypothesis : identifier -> goal sigma -> bool exception Bound -(*s Primitive tactics. *) +(** {6 Primitive tactics. } *) val introduction : identifier -> tactic val refine : constr -> tactic @@ -55,7 +52,7 @@ val fix : identifier option -> int -> tactic val mutual_cofix : identifier -> (identifier * constr) list -> int -> tactic val cofix : identifier option -> tactic -(*s Introduction tactics. *) +(** {6 Introduction tactics. } *) val fresh_id_in_env : identifier list -> identifier -> env -> identifier val fresh_id : identifier list -> identifier -> goal sigma -> identifier @@ -65,20 +62,21 @@ val intro : tactic val introf : tactic val intro_move : identifier option -> identifier move_location -> tactic - (* [intro_avoiding idl] acts as intro but prevents the new identifier + (** [intro_avoiding idl] acts as intro but prevents the new identifier to belong to [idl] *) val intro_avoiding : identifier list -> tactic val intro_replacing : identifier -> tactic val intro_using : identifier -> tactic val intro_mustbe_force : identifier -> tactic +val intro_then : (identifier -> tactic) -> 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 +(** [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 @@ -88,7 +86,7 @@ val intros_until : quantified_hypothesis -> tactic val intros_clearing : bool list -> tactic -(* Assuming a tactic [tac] depending on an hypothesis identifier, +(** 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 @@ -97,21 +95,21 @@ val intros_clearing : bool list -> tactic val try_intros_until : (identifier -> tactic) -> quantified_hypothesis -> tactic -(* Apply a tactic on a quantified hypothesis, an hypothesis in context +(** Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) val onInductionArg : (constr with_bindings -> tactic) -> constr with_bindings induction_arg -> tactic -(*s Introduction tactics with eliminations. *) +(** {6 Introduction tactics with eliminations. } *) val intro_pattern : identifier move_location -> intro_pattern_expr -> tactic val intro_patterns : intro_pattern_expr located list -> tactic val intros_pattern : identifier move_location -> intro_pattern_expr located list -> tactic -(*s Exact tactics. *) +(** {6 Exact tactics. } *) val assumption : tactic val exact_no_check : constr -> tactic @@ -119,7 +117,7 @@ val vm_cast_no_check : constr -> tactic val exact_check : constr -> tactic val exact_proof : Topconstr.constr_expr -> tactic -(*s Reduction tactics. *) +(** {6 Reduction tactics. } *) type tactic_reduction = env -> evar_map -> constr -> constr @@ -156,7 +154,7 @@ val pattern_option : val reduce : red_expr -> clause -> tactic val unfold_constr : global_reference -> tactic -(*s Modification of the local context. *) +(** {6 Modification of the local context. } *) val clear : identifier list -> tactic val clear_body : identifier list -> tactic @@ -169,7 +167,7 @@ val rename_hyp : (identifier * identifier) list -> tactic val revert : identifier list -> tactic -(*s Resolution tactics. *) +(** {6 Resolution tactics. } *) val apply_type : constr -> constr list -> tactic val apply_term : constr -> constr list -> tactic @@ -193,7 +191,7 @@ val apply_in : val simple_apply_in : identifier -> constr -> tactic -(*s Elimination tactics. *) +(** {6 Elimination tactics. } *) (* @@ -219,52 +217,52 @@ val simple_apply_in : identifier -> constr -> tactic Principles taken from functional induction have the final (f...). *) -(* [rel_contexts] and [rel_declaration] actually contain triples, and +(** [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_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 *) - 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) + 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 *) + 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) 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 *) + 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_bindings -> types -> elim_scheme val rebuild_elimtype_from_scheme: elim_scheme -> types -(* elim principle with the index of its inductive arg *) +(** elim principle with the index of its inductive arg *) type eliminator = { - elimindex : int option; (* None = find it automatically *) + elimindex : int option; (** None = find it automatically *) elimbody : constr with_bindings } -val elimination_clause_scheme : evars_flag -> - bool -> int -> clausenv -> clausenv -> tactic +val elimination_clause_scheme : evars_flag -> ?flags:unify_flags -> + int -> clausenv -> clausenv -> tactic -val elimination_in_clause_scheme : evars_flag -> identifier -> int -> - clausenv -> clausenv -> tactic +val elimination_in_clause_scheme : evars_flag -> ?flags:unify_flags -> + 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_bindings -> eliminator -> ?allow_K:bool -> tactic -val general_elim_in : evars_flag -> - identifier -> constr with_bindings -> eliminator -> tactic + constr with_bindings -> eliminator -> tactic +val general_elim_in : evars_flag -> identifier -> + constr with_bindings -> eliminator -> tactic val default_elim : evars_flag -> constr with_bindings -> tactic val simplest_elim : constr -> tactic @@ -273,37 +271,39 @@ val elim : val simple_induct : quantified_hypothesis -> tactic -val new_induct : evars_flag -> constr with_bindings induction_arg list -> +val new_induct : evars_flag -> + (evar_map * 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. *) +(** {6 Case analysis tactics. } *) 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_bindings induction_arg list -> +val new_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 -> clause option -> tactic -(*s Generic case analysis / induction tactics. *) +(** {6 Generic case analysis / induction tactics. } *) val induction_destruct : rec_flag -> evars_flag -> - (constr with_bindings induction_arg list * + ((evar_map * 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. *) +(** {6 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. *) +(** {6 Some eliminations which are frequently used. } *) val impE : identifier -> tactic val andE : identifier -> tactic @@ -313,7 +313,7 @@ val dAnd : clause -> tactic val dorE : bool -> clause ->tactic -(*s Introduction tactics. *) +(** {6 Introduction tactics. } *) val constructor_tac : evars_flag -> int option -> int -> constr bindings -> tactic @@ -332,7 +332,7 @@ val simplest_left : tactic val simplest_right : tactic val simplest_split : tactic -(*s Logical connective tactics. *) +(** {6 Logical connective tactics. } *) val register_setoid_reflexivity : tactic -> unit val reflexivity_red : bool -> tactic @@ -362,13 +362,15 @@ 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 -> constr -> types option -> clause -> tactic +val letin_pat_tac : (bool * intro_pattern_expr located) option -> name -> + evar_map * constr -> types option -> clause -> tactic val assert_tac : name -> types -> tactic val assert_by : name -> types -> tactic -> tactic val pose_proof : name -> constr -> tactic val generalize : constr list -> tactic val generalize_gen : ((occurrences * constr) * name) list -> tactic -val generalize_dep : ?with_let:bool (* Don't lose let bindings *) -> 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 @@ -382,3 +384,6 @@ val specialize_eqs : identifier -> tactic val register_general_multi_rewrite : (bool -> evars_flag -> constr with_bindings -> clause -> tactic) -> unit + +val register_subst_one : + (bool -> identifier -> identifier * constr * bool -> tactic) -> unit |