From 902da7d2949464ff54dafc3fda1d44365270d2e1 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 28 Apr 2014 13:47:25 +0200 Subject: Try a new way of handling template universe levels --- pretyping/evarsolve.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'pretyping/evarsolve.mli') diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 7276669bf..ca03f9853 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -34,7 +34,8 @@ type conv_fun_bool = val evar_define : conv_fun -> ?choose:bool -> ?dir:bool -> env -> evar_map -> bool option -> existential -> constr -> evar_map -val refresh_universes : bool -> evar_map -> types -> evar_map * types +val refresh_universes : ?all:bool (* Include domains of products *) -> + ?with_globals:bool -> bool -> evar_map -> types -> evar_map * types val solve_refl : ?can_drop:bool -> conv_fun_bool -> env -> evar_map -> bool option -> existential_key -> constr array -> constr array -> evar_map -- cgit v1.2.3