aboutsummaryrefslogtreecommitdiff
path: root/test-suite/misc/poly-capture-global-univs
AgeCommit message (Expand)Author
2019-07-02[test-suite] Fix evil plugin after changes in declare API.Emilio Jesus Gallego Arias
2019-06-24Duplicate the type of constant entries in Proof_global.Pierre-Marie Pédrot
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2018-11-09Use arrays of names instead of lists in abstract universe names.Pierre-Marie Pédrot
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-11-02gitignore test-suite/misc/poly-capture-global-univs/src/evil.mlGaëtan Gilbert
2018-10-19Porting the test-suite to coqpp.Pierre-Marie Pédrot
2018-09-13Add test for inconsistency from polymorphism capturing global univsGaëtan Gilbert