aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2019-11-27Display more information when complexity tests failJason Gross
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
2019-11-27Merge PR #11128: Fix #11039: proof of False with template poly and nonlinear ...Pierre-Marie Pédrot
2019-11-26Merge PR #11177: Add a complexity test for `pattern`Hugo Herbelin
2019-11-26Remove `rapply` tactic notation in favor of just the tacticJason Gross
2019-11-26Make rapply handle all numbers of underscoresJason Gross
2019-11-26Update test-suite/complexity/pattern.vJason Gross
2019-11-26Merge PR #11090: Printing of coercions to which a notation is associated: a r...Emilio Jesus Gallego Arias
2019-11-26Merge PR #11166: Add test for #11161Emilio Jesus Gallego Arias
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
2019-11-25Merge PR #11146: Combine similar arguments when printing Arguments commandHugo Herbelin
2019-11-25Test-suite: avoid using “omega”Vincent Laporte
2019-11-25Add a complexity test for `pattern`Jason Gross
2019-11-22Add test for #11161Gaëtan Gilbert
2019-11-21A refined version of #8890 which prevents #11033.Hugo Herbelin
2019-11-21Merge PR #11132: Fixing bugs in the computation of implicit arguments for `Fi...Emilio Jesus Gallego Arias
2019-11-21Merge PR #11075: load .vo when .vos is missing + misc vos changesEmilio Jesus Gallego Arias
2019-11-20Combine similar arguments when printing Arguments commandGaëtan Gilbert
2019-11-20From CoqIDE or -vos or -vok compilation, load .vo when .vos is missing (fixin...charguer
2019-11-19Fixing bugs in the computation of implicit arguments for fix with a let binder.Hugo Herbelin
2019-11-13Return of Refine Instance as an attribute.Gaëtan Gilbert
2019-11-13Merge PR #11094: Miscellaneous micro-improvements of the syntax of recordsPierre-Marie Pédrot
2019-11-12Merge PR #11045: Forbid Include inside sectionsPierre-Marie Pédrot
2019-11-11Run update-compat script with --release option.Théo Zimmermann
2019-11-11Merge PR #11052: Fix #11048: uncaught destKO in inductive typePierre-Marie Pédrot
2019-11-11Miscellaneous improvements of the syntax of records.Hugo Herbelin
2019-11-10Merge PR #10980: Fix #10903: type-in-type allows fixpoints on sprop inductivesPierre-Marie Pédrot
2019-11-08Merge PR #11014: Fix #8459: anomaly not enough abstractions in fix bodyPierre-Marie Pédrot
2019-11-07Merge PR #11049: Prevent redefinition of Ltac2 types and constructors inside ...Pierre-Marie Pédrot
2019-11-06Swap parsing precedence of `::` and `,` ; Fix #10116Kenji Maillard
2019-11-05Fixing test-suiteKenji Maillard
2019-11-05Fix #11048: uncaught destKO in inductive typeGaëtan Gilbert
2019-11-05Forbid Include inside sectionsGaëtan Gilbert
2019-11-04Prevent double definition of Ltac2 constructors inside a module; Fix #11046Kenji Maillard
2019-11-04Prevent redefinition of Ltac2 types; fix #10097Kenji Maillard
2019-11-01Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) r...Enrico Tassi
2019-11-01Merge PR #9867: Add primitive floats (binary64 floating-point numbers)Maxime Dénès
2019-11-01Merge PR #8642: Compiled interfaces with -vos and -vok optionsPierre-Marie Pédrot
2019-11-01Merge PR #11019: enforcing Ltac2 constructor name are uppercasedPierre-Marie Pédrot
2019-11-01adding test file for Uppercase Ltac2 constructorsKenji Maillard
2019-11-01[test-suite] acknowledge coq_mafile installs .vosEnrico Tassi
2019-11-01Implementing support for vos/vok files.charguer
2019-11-01Add extraction for primitive floatsErik Martin-Dorel
2019-11-01Fix ldshiftexpPierre Roux
2019-11-01Add "==", "<", "<=" in PrimFloat.vErik Martin-Dorel
2019-11-01Make primitive float work on WindowsPierre Roux
2019-11-01Make primitive float work on x86_32Pierre Roux
2019-11-01Pretty-printing primitive float constantsErik Martin-Dorel
2019-11-01Parsing primitive float constantsPierre Roux
2019-11-01Add tests for primitive floats with 'native_compute'Pierre Roux
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 11:23:22 +0000