summaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2020-04-03Merge PR #11995: Enable Async proofs using `Set Default Proof` annotationsPierre-Marie Pédrot
2020-04-02Fix #11941: anomaly in equality schemesGaëtan Gilbert
2020-04-01[stm] Use Default Proof Using only with Proofrefs/pull/11995/headTej Chajed
2020-03-31Print a warning when parsing non floating-point values.refs/pull/11975/headPierre Roux
2020-03-26Fix #11845: anomaly when including partially applied functorGaëtan Gilbert
2020-03-26Properly thread let-bindings in Funind principle construction.Pierre-Marie Pédrot
2020-03-20test coq-makefile/findlib-package-unpacked: only try to invoke 'make' whenRalf Treinen
2020-03-20test coq-makefile/camldep: try to build a cmx only when there is an ocamloptRalf Treinen
2020-03-20Add test for PR11811 (disable a positivity check)SimonBoulier
2020-03-20Fixes #11692 (clear dependent knows about let-in).Hugo Herbelin
2020-03-11Fix #11730: Mangle Names vs InfixGaëtan Gilbert
2020-03-11Fix #9930: "change" replaces 0-param projections by constantsGaëtan Gilbert
2020-03-10Be robust in calculating visible ids for non-registered constants.Pierre-Marie Pédrot
2020-03-10Fixing little bug in parsing decimal numbers in R.Hugo Herbelin
2020-03-02Makefile in test-suite: More separation of concerns as suggested by Enrico.Hugo Herbelin
2020-03-02Fixed some escaping problems with arguments containing spaces in IDE's Compil...Ike Mulder
2020-02-26Fix #11552: Ltac2 breaks query commands during proofs.Pierre-Marie Pédrot
2020-02-26Fix #11549: Ltac2 is incompatible with $.Pierre-Marie Pédrot
2020-02-26Merge PR #11613: Fixes custom entries precedence bugs for 8.11 (#11331, #9519...Pierre-Marie Pédrot
2020-02-24Fixing #11114 (anomaly with Extraction Implicit on records).Hugo Herbelin
2020-02-24Fixes #10917 (missing lift in building return clause by inversion).Hugo Herbelin
2020-02-24Fixing bug #9521 (anomaly due to missing declaration of level in custom entry).Hugo Herbelin
2020-02-24Fixes #11331 (unexpected level collisions between custom entries and constr).Hugo Herbelin
2020-02-12Fix #11515: Ltac2 rewrite on wildcard.Pierre-Marie Pédrot
2020-02-12Fix #11553: magicaly_constant_of_fixbody checks existence of made up constantGaëtan Gilbert
2020-01-29Fix #11467Pierre Roux
2020-01-22Fix #11421 computation of Set+2Gaëtan Gilbert
2020-01-20[zify] quick fix of #11191refs/pull/11430/headFrédéric Besson
2020-01-14[coqdoc] Fix #11353: coqdoc -g omits all sentences with decorationsKarl Palmskog
2020-01-13fix #11279. Specialize h no longer expands letins in the type of h.Pierre Courtieu
2020-01-13replace deprecated -quick with -vio in the test suiteEnrico Tassi
2020-01-13Fix #11195 and add other improvements: try loading .vio (and not just .vo) if...charguer
2020-01-11Add non-utf8 timing testJason Gross
2020-01-08Fix #11140: Bidirectionality hints perform (surprising?) simplificationMaxime Dénès
2020-01-07Fix #11360: discharge of template inductive with param only use of varGaëtan Gilbert
2020-01-06Fixing status reporting for complexity tests.Hugo Herbelin
2020-01-04coq_makefile: test with CAMLPKGS and mllibGaëtan Gilbert
2020-01-04fix: Shorten ssrsetoid.vErik Martin-Dorel
2019-12-30Fixes #11231 (missing dependency in pattern-matching decompilation).Hugo Herbelin
2019-12-30Fixes a small bug exposing an _ANONYMOUS_REL in a unification error message.Hugo Herbelin
2019-12-28Add critical-bugs entry, tests-suite file, and code comment.Guillaume Melquiond
2019-12-27Ensure that a custom entry cannot be defined twice.Pierre-Marie Pédrot
2019-12-24Deprecate the "omega with *" syntax.refs/pull/11337/headPierre-Marie Pédrot
2019-12-23Fix #11303: skip complexity tests on windows even if bogomips foundrefs/pull/11330/headGaëtan Gilbert
2019-12-22Add test cases for #9490 and #9532Maxime Dénès
2019-12-19Make the string argument of `time` print correctlyJason Gross
2019-12-18[micromega] fix efficiency regressionFrédéric Besson
2019-12-17Fix refine and eapply to mark shelved goals as non-resolvable, alwaysMatthieu Sozeau
2019-12-12Fixing #10750 (anomaly of "Print Visibility" on only-printing notations).Hugo Herbelin
2019-12-12Fixing #9893 (Letins not supported in the specialized hypothesis).Pierre Courtieu
generated by cgit v0.10.2-6-g49f6 at 2024-05-10 14:42:01 (GMT)