aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/base_include
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-19 16:14:49 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-19 16:14:49 +0200
commita5722cc823dcf13594098dd21813feaaaf893bf0 (patch)
treef4c55edaab3701d35d02c50dc9e732c903902ea8 /dev/base_include
parentcd2af7f5dd96a639dbc531064d89de0ee82ef3e6 (diff)
parent89a85a6603b7112e685a052d728284d3e4c2881e (diff)
Merge PR #7491: Fix #7421: constr_eq ignores universe constraints.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions