diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 01d517c16..8765541b2 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -39,8 +39,8 @@ val inj_ebindings : constr bindings -> open_constr bindings (*s General functions. *) val string_of_inductive : constr -> string -val head_constr : constr -> constr list -val head_constr_bound : constr -> constr list -> constr list +val head_constr : constr -> constr * constr list +val head_constr_bound : constr -> constr * constr list val is_quantified_hypothesis : identifier -> goal sigma -> bool exception Bound |