diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-10 14:11:07 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-10 14:11:07 +0000 |
| commit | c5fa08bbecbc665e1d82d38d2e41f5256efcd545 (patch) | |
| tree | 28ca895d2615fce2041a7353d06451a9b1e742e8 /interp/constrintern.mli | |
| parent | 22f3c77a4fbd67eb1a453bab8fcc61e6aea508ce (diff) | |
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
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 97b0f4fd1..be78837ff 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) *) |