diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index d6e648b9b..c076efb1f 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -26,12 +26,13 @@ open Locus (** {6 General functions. } *) +exception Bound + val head_constr : constr -> constr val head_constr_bound : constr -> constr +val decompose_app_bound : constr -> global_reference * constr array val is_quantified_hypothesis : Id.t -> goal sigma -> bool -exception Bound - (** {6 Primitive tactics. } *) val introduction : Id.t -> tactic |