diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 9a2af0835..937efdae1 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -26,8 +26,8 @@ open Locus (** {6 General functions. } *) -val head_constr : constr -> constr * constr list -val head_constr_bound : constr -> constr * constr list +val head_constr : constr -> constr +val head_constr_bound : constr -> constr val is_quantified_hypothesis : Id.t -> goal sigma -> bool exception Bound @@ -45,6 +45,9 @@ val fix : Id.t option -> int -> tactic val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> tactic val cofix : Id.t option -> tactic +val convert : constr -> constr -> tactic +val convert_leq : constr -> constr -> tactic + (** {6 Introduction tactics. } *) val fresh_id_in_env : Id.t list -> Id.t -> env -> Id.t |