diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-26 11:05:00 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-26 11:05:00 +0200 |
| commit | 83ae5e6ad95372912ba9eb9f8c52d857cdf10021 (patch) | |
| tree | 6698ac68f45940456cafb56aaaf0dec36bfb408f /pretyping/evarsolve.mli | |
| parent | f6382ef326099651cd051aa907b4e9ac6c905698 (diff) | |
Change interface of refresh universes to get a pbty argument instead of
the computed direction argument. In case pbty is conv, no refreshing is done
as the evar body must be convertible with the given term, however refreshing
of template application evar arguments can still happen.
(Re)-Closing bug #2966.
Diffstat (limited to 'pretyping/evarsolve.mli')
| -rw-r--r-- | pretyping/evarsolve.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 6de8f5c8d..16a4aff5b 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -31,11 +31,11 @@ type conv_fun = type conv_fun_bool = env -> evar_map -> conv_pb -> constr -> constr -> bool -val evar_define : conv_fun -> ?choose:bool -> ?dir:bool -> env -> evar_map -> +val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> bool option -> existential -> constr -> evar_map val refresh_universes : ?onlyalg:bool (* Only algebraic universes *) -> - bool (* direction: true for levels lower than the existing levels *) -> + bool option (* direction: true for levels lower than the existing levels *) -> env -> evar_map -> types -> evar_map * types val solve_refl : ?can_drop:bool -> conv_fun_bool -> env -> evar_map -> |