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/typing.ml | |
| 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/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 2f34f7efe..7702355b8 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -290,7 +290,7 @@ let e_type_of ?(refresh=false) env evd c = let j = execute env evdref c in (* side-effect on evdref *) if refresh then - Evarsolve.refresh_universes false !evdref j.uj_type + Evarsolve.refresh_universes false env !evdref j.uj_type else !evdref, j.uj_type let solve_evars env evdref c = |