diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-03-05 16:03:47 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-03-11 11:04:45 +0100 |
| commit | 0cd0a3ecdc7f942da153c59369ca3572bd18dd10 (patch) | |
| tree | bc0da893f040205068263f3133f9793cdf405b06 /checker/mod_checking.ml | |
| parent | 64867e7f6a86867e45ddd052b82f51b1b0355c97 (diff) | |
Fix (3243): univ constraints of module subtyping were not propagated
Universe constraints coming from subtyping were not propagated
to the outermost module and hence not stocked in the .vo file.
Still, they were added to the interactive safe environment and
hence checked for satisfiability.
Diffstat (limited to 'checker/mod_checking.ml')
0 files changed, 0 insertions, 0 deletions