From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- contrib/subtac/subtac_command.mli | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'contrib/subtac/subtac_command.mli') 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 -- cgit v1.2.3