From cbf1315572bdb86dd5fc9102690f3585194bbc30 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 20 Jun 2014 12:29:04 +0200 Subject: Cleanup treatment of template universe polymorphism (thanks to E. Tassi for helping fixing this). Now the issue is handled solely through refreshing of the terms assigned to evars during unification. If ?X = list ?Y, then Y's type is refreshed so that it doesn't mention a template universe and in turn, ?X won't. Same goes when typechecking (nil ?X, nil ?Y), the pair constructor levels will be set higher than fresh universes for the lists carriers. This also handles user-defined functions on template polymorphic inductives, which was fragile before. Pretyping and Evd are now uncluttered from template-specific code. --- pretyping/evarsolve.mli | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'pretyping/evarsolve.mli') diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 23ed6a2ef..988938272 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -34,9 +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 : ?all:bool (* Include domains of products *) -> - ?template:bool -> (* Generate template fresh universe variables, to be instantiated eagerly *) - ?with_globals:bool -> bool -> evar_map -> types -> evar_map * types +val refresh_universes : bool (* 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 -> bool option -> existential_key -> constr array -> constr array -> evar_map -- cgit v1.2.3