diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-20 12:29:04 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-20 12:29:04 +0200 |
| commit | cbf1315572bdb86dd5fc9102690f3585194bbc30 (patch) | |
| tree | 9172ad81c7b9381e4ffd7aeeae5589493320cf0d /pretyping/evd.mli | |
| parent | 8b90dc406730123640f186c8b39f6329a3f434a4 (diff) | |
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.
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 14 |
1 files changed, 6 insertions, 8 deletions
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 |