diff options
Diffstat (limited to 'contrib/subtac/subtac_command.mli')
| -rw-r--r-- | contrib/subtac/subtac_command.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli index 27520867..3a6a351b 100644 --- a/contrib/subtac/subtac_command.mli +++ b/contrib/subtac/subtac_command.mli @@ -42,6 +42,7 @@ val interp_binder : Evd.evar_defs ref -> Environ.env -> Names.name -> Topconstr.constr_expr -> Term.constr + val build_recursive : (fixpoint_expr * decl_notation) list -> bool -> unit |