diff options
Diffstat (limited to 'contrib/subtac/subtac_command.mli')
| -rw-r--r-- | contrib/subtac/subtac_command.mli | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli index 846e06cf..27520867 100644 --- a/contrib/subtac/subtac_command.mli +++ b/contrib/subtac/subtac_command.mli @@ -14,18 +14,18 @@ val interp_gen : evar_defs ref -> env -> ?impls:full_implicits_env -> - ?allow_soapp:bool -> + ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> constr val interp_constr : evar_defs ref -> env -> constr_expr -> constr -val interp_type : +val interp_type_evars : evar_defs ref -> env -> ?impls:full_implicits_env -> constr_expr -> constr -val interp_casted_constr : +val interp_casted_constr_evars : evar_defs ref -> env -> ?impls:full_implicits_env -> @@ -38,5 +38,12 @@ val interp_constr_judgment : constr_expr -> unsafe_judgment val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list +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 + +val build_corecursive : + (cofixpoint_expr * decl_notation) list -> bool -> unit |