diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-20 22:30:37 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-12 10:39:33 +0200 |
| commit | b006f10e7d591417844ffa1f04eeb926d6092d7b (patch) | |
| tree | 9253b32cb1adabafce28f123ef9eb11d4fa122f4 /interp/constrintern.mli | |
| parent | ca300977724a6b065a98c025d400c71f41b9df4b (diff) | |
Uniformisation of the order of arguments env and sigma.
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index b5cad5d28..932c871e5 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -97,41 +97,41 @@ val intern_context : bool -> env -> internalization_env -> local_binder list -> (** Main interpretation functions expecting evars to be all resolved *) -val interp_constr : evar_map -> env -> ?impls:internalization_env -> +val interp_constr : env -> evar_map -> ?impls:internalization_env -> constr_expr -> constr Evd.in_evar_universe_context -val interp_casted_constr : evar_map -> env -> ?impls:internalization_env -> +val interp_casted_constr : env -> evar_map -> ?impls:internalization_env -> constr_expr -> types -> constr Evd.in_evar_universe_context -val interp_type : evar_map -> env -> ?impls:internalization_env -> +val interp_type : env -> evar_map -> ?impls:internalization_env -> constr_expr -> types Evd.in_evar_universe_context (** Main interpretation function expecting evars to be all resolved *) -val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr +val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr (** Accepting unresolved evars *) -val interp_constr_evars : evar_map ref -> env -> +val interp_constr_evars : env -> evar_map ref -> ?impls:internalization_env -> constr_expr -> constr -val interp_casted_constr_evars : evar_map ref -> env -> +val interp_casted_constr_evars : env -> evar_map ref -> ?impls:internalization_env -> constr_expr -> types -> constr -val interp_type_evars : evar_map ref -> env -> +val interp_type_evars : env -> evar_map ref -> ?impls:internalization_env -> constr_expr -> types (** Accepting unresolved evars and giving back the manual implicit arguments *) -val interp_constr_evars_impls : evar_map ref -> env -> +val interp_constr_evars_impls : env -> evar_map ref -> ?impls:internalization_env -> constr_expr -> constr * Impargs.manual_implicits -val interp_casted_constr_evars_impls : evar_map ref -> env -> +val interp_casted_constr_evars_impls : env -> evar_map ref -> ?impls:internalization_env -> constr_expr -> types -> constr * Impargs.manual_implicits -val interp_type_evars_impls : evar_map ref -> env -> +val interp_type_evars_impls : env -> evar_map ref -> ?impls:internalization_env -> constr_expr -> types * Impargs.manual_implicits @@ -149,25 +149,25 @@ val interp_reference : ltac_sign -> reference -> glob_constr (** Interpret binders *) -val interp_binder : evar_map -> env -> Name.t -> constr_expr -> +val interp_binder : env -> evar_map -> Name.t -> constr_expr -> types Evd.in_evar_universe_context -val interp_binder_evars : evar_map ref -> env -> Name.t -> constr_expr -> types +val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types (** Interpret contexts: returns extended env and context *) val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> - evar_map ref -> env -> local_binder list -> + env -> evar_map ref -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits) (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *) (* (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *) (* ?global_level:bool -> ?impl_env:internalization_env -> *) -(* evar_map -> env -> local_binder list -> internalization_env * ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *) +(* env -> evar_map -> local_binder list -> internalization_env * ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *) (* val interp_context : ?global_level:bool -> ?impl_env:internalization_env -> *) -(* evar_map -> env -> local_binder list -> *) +(* env -> evar_map -> local_binder list -> *) (* internalization_env * *) (* ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *) |