aboutsummaryrefslogtreecommitdiff
path: root/test-suite/coqchk/univ.v
AgeCommit message (Expand)Author
2018-05-24Fix #7323: coqchk puts polymorphic univs of inductive in global envGaëtan Gilbert
2018-04-23Fix #7327: coqchk subtyping of polymorphic constantsGaëtan Gilbert
2018-04-20Fix #6798: coqchk ignores ugraph when comparing constant instancesGaëtan Gilbert
2017-05-30Add test-suite checks for coqchk with constraintsJason Gross
2014-12-26new test for coqchkEnrico Tassi