aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
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
2019-11-01Add next_{up,down} primitive float functionsPierre Roux
2019-11-01Implement classify on primitive floatPierre Roux
2019-11-01Change return type of primitive float comparisonPierre Roux
2019-11-01Add tests for primitive floats with 'vm_compute'Guillaume Bertholon
2019-11-01Add tests for primitive floatsGuillaume Bertholon
2019-11-01[ssr] Refactor/Extend of under to support more relationsErik Martin-Dorel
2019-10-31[ssr] Refactor/Simplify the implementation of underErik Martin-Dorel
2019-10-31Merge PR #10985: Print argument info as an Arguments command in AboutEmilio Jesus Gallego Arias
2019-10-31Merge PR #9883: Add support for Sorts in numeral notationsVincent Laporte
2019-10-31restore red behaviour printingGaëtan Gilbert
2019-10-31Fix output testsGaëtan Gilbert
2019-10-31Merge PR #10861: Fix #10615: Notation substitution for Ltac2 terms.Gaëtan Gilbert
2019-10-31Fix #8459: anomaly not enough abstractions in fix bodyGaëtan Gilbert
2019-10-31Merge PR #10995: add test for #4502 (fixed by unknown commit)Pierre-Marie Pédrot
2019-10-30[test-suite] Test section-local mutual Fixpoint.Emilio Jesus Gallego Arias
2019-10-30Merge PR #10973: Remove dead code in save_remaining_recthmsEmilio Jesus Gallego Arias
2019-10-30add test for #4502 (fixed by unknown commit)Gaëtan Gilbert
2019-10-30Merge PR #10494: Show diffs in "Show Proof."Enrico Tassi
2019-10-29Show diffs in "Show Proof."Jim Fehrle
2019-10-29Fix #9114, assert_succeeds (exact I) solves goalJason Gross
2019-10-29`assert_succeeds`&`assert_fails`: multisuccess fixJason Gross
2019-10-29Fix #10615: Notation substitution for Ltac2 terms.Pierre-Marie Pédrot
2019-10-28Add support for Sorts in numeral notationsJason Gross
2019-10-28Fix #10903: type-in-type allows fixpoints on sprop inductivesGaëtan Gilbert
2019-10-27Merge PR #10827: Replace classical reals quotient axioms by functional extens...Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-03 17:56:38 +0000