diff options
| author | Matthieu Sozeau | 2014-04-07 12:53:41 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:58 +0200 |
| commit | 105db906ae45e792d1caeeb2e3fb7f69944b2caa (patch) | |
| tree | b12ca28e6b172d2524c6a11c851c7d568f6a2411 /pretyping/evarsolve.ml | |
| parent | b17c1e128fad2e84ebe4e4742b47bd67d88c56d6 (diff) | |
- Fixes for canonical structure resolution (check that the initial term indeed unifies
with the projected term, keeping track of universes).
- Fix the [unify] tactic to fail properly.
- Fix unification to disallow lowering a global Type(i) universe to Prop or Set.
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 306116d76d..761f11c115 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -30,8 +30,8 @@ let refresh_universes dir evd t = let evdref = ref evd in let modified = ref false in let rec refresh t = match kind_of_term t with - | Sort (Type u as s) when Univ.universe_level u = None || - Evd.is_sort_variable evd s = None -> + | Sort (Type u as s) when Univ.universe_level u = None + (* || Evd.is_sort_variable evd s = None *) -> (modified := true; (* s' will appear in the term, it can't be algebraic *) let s' = evd_comb0 (new_sort_variable Evd.univ_flexible) evdref in |