diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-25 13:08:17 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-25 13:08:17 +0200 |
| commit | b354b232c3356159f6866fab00816cd5412cd036 (patch) | |
| tree | fc35107753dec3ce13389a613f9fce0fc9cf9be1 /library/goptions.ml | |
| parent | fae911a7ac35150997c7c0b21ffe219d80dd5f93 (diff) | |
In exact check, use e_type_of to ensure that universe constraints necessary
to typecheck the term are not forgotten. (relieves tactic implementors from
calling e_type_of themselves, e.g. in congruence). Fixes a bug found in Containers.
Diffstat (limited to 'library/goptions.ml')
0 files changed, 0 insertions, 0 deletions