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/evd.mli | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) (limited to 'pretyping/evd.mli') diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 1393a33d3..b6db3c263 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -261,7 +261,6 @@ val drop_side_effects : evar_map -> evar_map Evar maps also keep track of the universe constraints defined at a given point. This section defines the relevant manipulation functions. *) -val is_sort_variable : evar_map -> sorts -> bool val whd_sort_variable : evar_map -> constr -> constr val set_leq_sort : evar_map -> sorts -> sorts -> evar_map val set_eq_sort : evar_map -> sorts -> sorts -> evar_map @@ -438,16 +437,15 @@ val normalize_evar_universe_context_variables : evar_universe_context -> val normalize_evar_universe_context : evar_universe_context -> evar_universe_context -val new_univ_level_variable : ?template:bool -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level -val new_univ_variable : ?template:bool -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe -val new_sort_variable : ?template:bool -> ?name:string -> rigid -> evar_map -> evar_map * sorts +val new_univ_level_variable : ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level +val new_univ_variable : ?name:string -> rigid -> evar_map -> evar_map * Univ.universe +val new_sort_variable : ?name:string -> rigid -> evar_map -> evar_map * sorts val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map -val is_sort_variable : evar_map -> sorts -> (Univ.universe_level * bool) option -(** [is_sort_variable evm s] returns [Some (u, is_rigid)] or [None] if [s] is - not a sort variable declared in [evm] *) +val is_sort_variable : evar_map -> sorts -> Univ.universe_level option +(** [is_sort_variable evm s] returns [Some u] or [None] if [s] is + not a local sort variable declared in [evm] *) val is_flexible_level : evar_map -> Univ.Level.t -> bool - val whd_sort_variable : evar_map -> constr -> constr (* val normalize_universe_level : evar_map -> Univ.universe_level -> Univ.universe_level *) val normalize_universe : evar_map -> Univ.universe -> Univ.universe -- cgit v1.2.3