aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2019-03-14Documentation for SPropGaëtan Gilbert
2019-03-14Test for SkySkimmer/coq#13Gaëtan Gilbert
2019-03-14Repair relevance marks in-kernel.Gaëtan Gilbert
2019-03-14Enable proof irrelevance for SProp.Gaëtan Gilbert
2019-03-14Inductives in SProp, forbid primitive records with only sprop fieldsGaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-03-14Fix Require in output test for reals syntaxGaëtan Gilbert
2019-03-13Merge PR #9736: Don't coqchk the test suite prerequisitesEnrico Tassi
2019-03-12Merge PR #9632: Fix #9631: Instance: anomaly grounding non evar-free termEmilio Jesus Gallego Arias
2019-03-12Merge PR #9596: Fix #9595: missing non-primitive-record warning with 0 field ...Emilio Jesus Gallego Arias
2019-03-12Merge PR #9389: Implement a method for manual declaration of implicits.Emilio Jesus Gallego Arias
2019-03-11Don't coqchk the test suite prerequisitesGaëtan Gilbert
2019-03-05Remove regularly failing test from test-suite.Théo Zimmermann
2019-03-04Merge PR #9688: [stm] unfocus when edition exits the proof (fix #9431)Emilio Jesus Gallego Arias
2019-03-04[stm] unfocus when edition exits the proof (fix #9431)Enrico Tassi
2019-03-01Set COQLIB so the test suite will run locally on Windows.Jim Fehrle
2019-02-28Implement a method for manual declaration of implicits.Jasper Hugunin
2019-02-26Fix #9526: Registering inductives for primitive integers doesn't check enoughMaxime Dénès
2019-02-25Fix #9631: Instance: anomaly grounding non evar-free termGaëtan Gilbert
2019-02-22Merge PR #9364: Apply implicit binders to Hypothesis inside sections.Gaëtan Gilbert
2019-02-22Merge PR #9576: [library] Remove `-boot` option.Enrico Tassi
2019-02-22Apply implicit binders to Hypothesis inside sections.Jasper Hugunin
2019-02-22Merge PR #9314: Enrich implicits for instancesGaëtan Gilbert
2019-02-22[library] Remove `-boot` option.Emilio Jesus Gallego Arias
2019-02-20[azure] [ci] Build on Windows using Dune.Emilio Jesus Gallego Arias
2019-02-19Merge PR #9297: Two fixes in printing notations with patternsEmilio Jesus Gallego Arias
2019-02-19Notations: Fixing a printing bug with patterns.Hugo Herbelin
2019-02-19Notations: Enforce strong evaluation of cases_pattern_of_glob_constr.Hugo Herbelin
2019-02-19Fix #9595: missing non-primitive-record warning with 0 field recordGaëtan Gilbert
2019-02-18Merge PR #9306: Remove Printing Primitive Projection CompatibilityMaxime Dénès
2019-02-18Merge PR #9142: Disable Ltac backtracesHugo Herbelin
2019-02-18Merge PR #9439: Separate variance and universe fields in inductives.Pierre-Marie Pédrot
2019-02-18Merge PR #9509: Fix #9508: Unexpected interaction between implicit arguments ...Maxime Dénès
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-17Merge PR #9528: Fix #9527: unknown evar in nonterminating [fix] error.Pierre-Marie Pédrot
2019-02-14Merge PR #9502: Remove nondeterministic testsThéo Zimmermann
2019-02-13Merge PR #9554: Don't save expected failure logs from opened/ bugs.Maxime Dénès
2019-02-13more testsEnrico Tassi
2019-02-13Fix #9432: canonical structure and coercion accept universe binders.Gaëtan Gilbert
2019-02-11Merge PR #9540: [ssr] keep user annotation on views (fix #9538)Cyril Cohen
2019-02-11Don't save expected failure logs from opened/ bugs.Gaëtan Gilbert
2019-02-11Fix #9508: Unexpected interaction between implicit arguments and primitive pr...Pierre-Marie Pédrot
2019-02-11Fix #9527: unknown evar in nonterminating [fix] error.Gaëtan Gilbert
2019-02-11[ssr] keep user annotation on views (fix #9538)Enrico Tassi
2019-02-08[test-suite] Improve test for async workers.Emilio Jesus Gallego Arias
2019-02-08[stm] Filter some more arguments that shouldn't be sent to workers.Emilio Jesus Gallego Arias
2019-02-08Merge PR #9410: Make `Program` a regular attributeMatthieu Sozeau
2019-02-07Merge PR #9477: Makefiles: Fixes for byte compilationEnrico Tassi
2019-02-07Remove nondeterministic testsGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 06:55:32 +0000