diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 25 |
1 files changed, 13 insertions, 12 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 354ac50b4..ba4a9706d 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -9,6 +9,7 @@ open Loc open Names open Term +open EConstr open Environ open Proof_type open Evd @@ -28,15 +29,15 @@ open Locus (** {6 General functions. } *) -val is_quantified_hypothesis : Id.t -> ([`NF],'b) Proofview.Goal.t -> bool +val is_quantified_hypothesis : Id.t -> ('a, 'r) Proofview.Goal.t -> bool (** {6 Primitive tactics. } *) val introduction : ?check:bool -> Id.t -> unit Proofview.tactic val convert_concl : ?check:bool -> types -> cast_kind -> unit Proofview.tactic -val convert_hyp : ?check:bool -> Context.Named.Declaration.t -> unit Proofview.tactic +val convert_hyp : ?check:bool -> named_declaration -> unit Proofview.tactic val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic -val convert_hyp_no_check : Context.Named.Declaration.t -> unit Proofview.tactic +val convert_hyp_no_check : named_declaration -> unit Proofview.tactic val mutual_fix : Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic val fix : Id.t option -> int -> unit Proofview.tactic @@ -50,7 +51,7 @@ val convert_leq : constr -> constr -> unit Proofview.tactic val fresh_id_in_env : Id.t list -> Id.t -> env -> Id.t val fresh_id : Id.t list -> Id.t -> goal sigma -> Id.t -val find_intro_names : Context.Rel.t -> goal sigma -> Id.t list +val find_intro_names : rel_context -> goal sigma -> Id.t list val intro : unit Proofview.tactic val introf : unit Proofview.tactic @@ -74,7 +75,7 @@ val intros : unit Proofview.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 -> ([`NF],'b) Proofview.Goal.t -> int + bool -> quantified_hypothesis -> ('a, 'r) Proofview.Goal.t -> int val intros_until : quantified_hypothesis -> unit Proofview.tactic @@ -184,7 +185,7 @@ val revert : Id.t list -> unit Proofview.tactic (** {6 Resolution tactics. } *) val apply_type : constr -> constr list -> unit Proofview.tactic -val bring_hyps : Context.Named.t -> unit Proofview.tactic +val bring_hyps : named_context -> unit Proofview.tactic val apply : constr -> unit Proofview.tactic val eapply : constr -> unit Proofview.tactic @@ -243,15 +244,15 @@ type elim_scheme = { elimc: constr with_bindings option; elimt: types; indref: global_reference option; - params: Context.Rel.t; (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) + params: rel_context; (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) nparams: int; (** number of parameters *) - predicates: Context.Rel.t; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) + predicates: rel_context; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) npredicates: int; (** Number of predicates *) - branches: Context.Rel.t; (** branchr,...,branch1 *) + branches: rel_context; (** branchr,...,branch1 *) nbranches: int; (** Number of branches *) - args: Context.Rel.t; (** (xni, Ti_ni) ... (x1, Ti_1) *) + args: rel_context; (** (xni, Ti_ni) ... (x1, Ti_1) *) nargs: int; (** number of arguments *) - indarg: Context.Rel.Declaration.t 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...) are optional and mutually exclusive *) @@ -259,7 +260,7 @@ type elim_scheme = { 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 compute_elim_sig : evar_map -> ?elimc:constr with_bindings -> types -> elim_scheme (** elim principle with the index of its inductive arg *) type eliminator = { |