From c5fa08bbecbc665e1d82d38d2e41f5256efcd545 Mon Sep 17 00:00:00 2001 From: pboutill Date: Thu, 10 Feb 2011 14:11:07 +0000 Subject: Interp a definition with the implicit arguments of its local context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13825 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/constrintern.mli | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'interp/constrintern.mli') diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 97b0f4fd1d..be78837ff3 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -82,7 +82,7 @@ val intern_pattern : env -> cases_pattern_expr -> Names.identifier list * ((Names.identifier * Names.identifier) list * Glob_term.cases_pattern) list -val intern_context : bool -> evar_map -> env -> local_binder list -> glob_binder list +val intern_context : bool -> evar_map -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list (** {6 Composing internalization with pretyping } *) @@ -152,14 +152,14 @@ val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types val interp_context_gen : (env -> glob_constr -> types) -> (env -> glob_constr -> unsafe_judgment) -> - ?global_level:bool -> - evar_map -> env -> local_binder list -> (env * rel_context) * Impargs.manual_implicits + ?global_level:bool -> ?impl_env:internalization_env -> + evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits) -val interp_context : ?global_level:bool -> - evar_map -> env -> local_binder list -> (env * rel_context) * Impargs.manual_implicits +val interp_context : ?global_level:bool -> ?impl_env:internalization_env -> + evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits) -val interp_context_evars : ?global_level:bool -> - evar_map ref -> env -> local_binder list -> (env * rel_context) * Impargs.manual_implicits +val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> + evar_map ref -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits) (** Locating references of constructions, possibly via a syntactic definition (these functions do not modify the glob file) *) -- cgit v1.2.3