aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
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
2019-02-06Avoid eqn when generating name in induction_gen.Jasper Hugunin
2019-02-06Makefiles: Fixes for byte compilationGaëtan Gilbert
2019-02-05Unset the Ltac backtrace printing by default.Pierre-Marie Pédrot
2019-02-05Make Program a regular attributeMaxime Dénès
2019-02-04Enrich implicits for instancesJasper Hugunin
2019-02-04[dune] Fix Dune build in Windows.Emilio Jesus Gallego Arias
2019-02-04Merge PR #6914: Primitive integersPierre-Marie Pédrot
2019-02-04Merge PR #9317: Restrict universes in records.Pierre-Marie Pédrot
2019-02-04Primitive integersMaxime Dénès
2019-02-04Merge PR #9368: Discard argument names of section variables on section closePierre-Marie Pédrot
2019-02-04Merge PR #8690: [toplevel] Split interactive toplevel and compiler binaries.Maxime Dénès
2019-02-04Merge PR #9426: [test-suite] Fix display of check.Enrico Tassi
2019-02-04Merge PR #9454: Fix off-by-one error in nat syntax warningsPierre-Marie Pédrot
2019-02-04Merge PR #9452: [proof] optimize proof always works on incomplete proofsPierre-Marie Pédrot
2019-02-04Merge PR #9291: Do not take universes into account in lia reification.Frédéric Besson
2019-02-02Merge PR #9250: coqchk: fix check for kelim with functorsPierre-Marie Pédrot
2019-02-01Merge PR #8062: Add Z.div_mod_to_quot_rem tactic, put it in zifyVincent Laporte
2019-02-01[toplevel] Split interactive toplevel and compiler binaries.Emilio Jesus Gallego Arias
2019-01-31Fix off-by-one error in nat syntax warningsJason Gross
2019-01-31add testEnrico Tassi
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
2019-01-30Restrict universes in records.Gaëtan Gilbert
2019-01-29Update update-compat.py scriptJason Gross
2019-01-29Merge PR #9274: Make `Instance` without a body always open a proofEnrico Tassi
2019-01-29[test-suite] Display full paths on CHECK.Emilio Jesus Gallego Arias
2019-01-29Merge PR #9383: Remove travisVincent Laporte
2019-01-29[test-suite] Fix display of check.Emilio Jesus Gallego Arias
2019-01-28Merge PR #9341: [ssr] uniform clear disciplineMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 06:34:02 +0000