aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-06-04 15:50:55 +0200
committerPierre-Marie Pédrot2019-06-06 17:50:48 +0200
commit738a753fc86efc3e98f08f1aa684cf2229194b09 (patch)
treec9744bb5e8901b22081a4f90c32ebac57c10e67f /dev
parent281faca10d471be5fd2bca864ffd382d69f7a110 (diff)
Merge the two sources of monomorphic constraints for side-effects.
Instead of having the monormorphic universes from the immediate data separated from the ones from the body, we only rely on the former. There is no reason to delay given that the body is always force upfront.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions