diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-13 05:51:36 +0530 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-13 05:51:36 +0530 |
| commit | 098781a2a1885a4f8768518a94b5026de9d375e6 (patch) | |
| tree | 711fd05e03101239048ef9e86c0132fee2f3bb21 /checker/values.ml | |
| parent | c60f40ccecf526b5c7ce5adfe5908fdac3f66771 (diff) | |
Fix bug when discharging universe constraints coming from variables
into monomorphic constants, which was still using the de Bruijn encoding
Bug revealed by discharging of hidden internal monomorphic definition in
otherwise polymorphic developments. Makes coqchk work on Hurkens again.
Diffstat (limited to 'checker/values.ml')
0 files changed, 0 insertions, 0 deletions