diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-10 14:10:51 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-10 14:10:51 +0000 |
| commit | 659795aeb2cd329eab5c4a92adbde724573dd106 (patch) | |
| tree | 433b5d3f8d525eeb18d79a8240507811612773d6 /interp/constrintern.mli | |
| parent | c24849ef42adda2c5792f02a2c04f75505a7002a (diff) | |
More comments and less doublons in some mli
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13820 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 59afcd313..12dc6be16 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -64,8 +64,6 @@ val compute_internalization_env : env -> var_internalization_type -> identifier list -> types list -> Impargs.manual_explicitation list list -> internalization_env -type manual_implicits = (explicitation * (bool * bool * bool)) list - type ltac_sign = identifier list * unbound_ltac_var_map type glob_binder = (name * binding_kind * glob_constr option * glob_constr) @@ -112,15 +110,15 @@ val interp_casted_constr : evar_map -> env -> ?impls:internalization_env -> (** Accepting evars and giving back the manual implicits in addition. *) val interp_casted_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env -> - ?impls:internalization_env -> constr_expr -> types -> constr * manual_implicits + ?impls:internalization_env -> constr_expr -> types -> constr * Impargs.manual_implicits val interp_type_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env -> ?impls:internalization_env -> - constr_expr -> types * manual_implicits + constr_expr -> types * Impargs.manual_implicits val interp_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env -> ?impls:internalization_env -> - constr_expr -> constr * manual_implicits + constr_expr -> constr * Impargs.manual_implicits val interp_casted_constr_evars : evar_map ref -> env -> ?impls:internalization_env -> constr_expr -> types -> constr @@ -155,13 +153,13 @@ 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) * manual_implicits + evar_map -> env -> local_binder list -> (env * rel_context) * Impargs.manual_implicits val interp_context : ?global_level:bool -> - evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits + evar_map -> env -> local_binder list -> (env * rel_context) * Impargs.manual_implicits val interp_context_evars : ?global_level:bool -> - evar_map ref -> env -> local_binder list -> (env * rel_context) * manual_implicits + evar_map ref -> env -> local_binder list -> (env * rel_context) * Impargs.manual_implicits (** Locating references of constructions, possibly via a syntactic definition (these functions do not modify the glob file) *) |