diff options
| author | Maxime Dénès | 2017-12-18 09:36:50 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-18 09:36:50 +0100 |
| commit | 0168ee0b6463a9ef44d768b0020b34785986c1cb (patch) | |
| tree | c3bb1d2eef4fa5edfd2d431669015db896e08633 /API | |
| parent | 50bd89748af03bb28ad7024f2ceef500489a91b0 (diff) | |
| parent | 53f5cc210da4debd5264d6d8651a76281b0b4256 (diff) | |
Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.mli | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/API/API.mli b/API/API.mli index 8f46a58321..6326247f81 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4620,6 +4620,9 @@ end module Constrintern : sig + + open Evd + type ltac_sign = { ltac_vars : Names.Id.Set.t; ltac_bound : Names.Id.Set.t; @@ -4635,11 +4638,11 @@ sig | Variable type internalization_env = var_internalization_data Names.Id.Map.t - val interp_constr_evars : Environ.env -> Evd.evar_map ref -> - ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.constr + val interp_constr_evars : Environ.env -> evar_map -> + ?impls:internalization_env -> Constrexpr.constr_expr -> evar_map * EConstr.constr - val interp_type_evars : Environ.env -> Evd.evar_map ref -> - ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.types + val interp_type_evars : Environ.env -> Evd.evar_map -> + ?impls:internalization_env -> Constrexpr.constr_expr -> evar_map * EConstr.types val empty_ltac_sign : ltac_sign val intern_gen : Pretyping.typing_constraint -> Environ.env -> @@ -4657,10 +4660,12 @@ sig val locate_reference : Libnames.qualid -> Globnames.global_reference val interp_type : Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> Constr.types Evd.in_evar_universe_context + val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> - Environ.env -> Evd.evar_map ref -> Constrexpr.local_binder_expr list -> - internalization_env * ((Environ.env * EConstr.rel_context) * Impargs.manual_implicits) + Environ.env -> Evd.evar_map -> Constrexpr.local_binder_expr list -> + evar_map * (internalization_env * ((Environ.env * EConstr.rel_context) * Impargs.manual_implicits)) + val compute_internalization_data : Environ.env -> var_internalization_type -> Constr.types -> Impargs.manual_explicitation list -> var_internalization_data val empty_internalization_env : internalization_env |