open Pretyping open Evd open Environ open Term open Topconstr open Names open Libnames open Pp open Vernacexpr open Constrintern val interp_gen : typing_constraint -> evar_map ref -> env -> ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> constr val interp_constr : evar_map ref -> env -> constr_expr -> constr val interp_type_evars : evar_map ref -> env -> ?impls:full_internalization_env -> constr_expr -> constr val interp_casted_constr_evars : evar_map ref -> env -> ?impls:full_internalization_env -> constr_expr -> types -> constr val interp_open_constr : evar_map ref -> env -> constr_expr -> constr val interp_constr_judgment : evar_map ref -> env -> constr_expr -> unsafe_judgment val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list val interp_binder : Evd.evar_map ref -> Environ.env -> Names.name -> Topconstr.constr_expr -> Term.constr val telescope : (Names.name * 'a option * Term.types) list -> Term.types * (Names.name * Term.types option * Term.types) list * Term.constr val build_wellfounded : Names.identifier * 'a * Topconstr.local_binder list * Topconstr.constr_expr * Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr -> 'b -> 'c -> Subtac_obligations.progress val build_recursive : (fixpoint_expr * decl_notation list) list -> bool -> unit val build_corecursive : (cofixpoint_expr * decl_notation list) list -> bool -> unit