diff options
| author | Matthieu Sozeau | 2019-02-08 10:44:23 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-02-08 10:44:23 +0100 |
| commit | d1d32f552064b9907fc9815b7412b9a9cde4a0dd (patch) | |
| tree | c4a4b20e92547abae487f8bb1115ba34382f0bfd /interp/constrintern.mli | |
| parent | 79b6317f738b6d2d7fdaaaad2cef79a092ec8c77 (diff) | |
| parent | 40ed1b7c5e94f418f9b758ffe1a86e4ad7743267 (diff) | |
Merge PR #9410: Make `Program` a regular attribute
Ack-by: SkySkimmer
Reviewed-by: aspiwack
Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: mattam82
Ack-by: maximedenes
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 61acd09d65..2d14a0d0a7 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -113,26 +113,26 @@ val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr (** Accepting unresolved evars *) -val interp_constr_evars : env -> evar_map -> +val interp_constr_evars : ?program_mode:bool -> env -> evar_map -> ?impls:internalization_env -> constr_expr -> evar_map * constr -val interp_casted_constr_evars : env -> evar_map -> +val interp_casted_constr_evars : ?program_mode:bool -> env -> evar_map -> ?impls:internalization_env -> constr_expr -> types -> evar_map * constr -val interp_type_evars : env -> evar_map -> +val interp_type_evars : ?program_mode:bool -> env -> evar_map -> ?impls:internalization_env -> constr_expr -> evar_map * types (** Accepting unresolved evars and giving back the manual implicit arguments *) -val interp_constr_evars_impls : env -> evar_map -> +val interp_constr_evars_impls : ?program_mode:bool -> env -> evar_map -> ?impls:internalization_env -> constr_expr -> evar_map * (constr * Impargs.manual_implicits) -val interp_casted_constr_evars_impls : env -> evar_map -> +val interp_casted_constr_evars_impls : ?program_mode:bool -> env -> evar_map -> ?impls:internalization_env -> constr_expr -> types -> evar_map * (constr * Impargs.manual_implicits) -val interp_type_evars_impls : env -> evar_map -> +val interp_type_evars_impls : ?program_mode:bool -> env -> evar_map -> ?impls:internalization_env -> constr_expr -> evar_map * (types * Impargs.manual_implicits) @@ -158,7 +158,7 @@ val interp_binder_evars : env -> evar_map -> Name.t -> constr_expr -> evar_map * (** Interpret contexts: returns extended env and context *) val interp_context_evars : - ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> + ?program_mode:bool -> ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> env -> evar_map -> local_binder_expr list -> evar_map * (internalization_env * ((env * rel_context) * Impargs.manual_implicits)) |