aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2018-10-31Merge PR #8759: Fix #8755: Uncaught exception Ltac_plugin.Taccoerce.CannotCoe...Hugo Herbelin
2018-10-31Notations: fixing a bug with abbreviations in custom entries.Hugo Herbelin
2018-10-29Fix for bug #8848Matthieu Sozeau
2018-10-29Merge PR #8737: Correctly report non-projection fields in recordsPierre-Marie Pédrot
2018-10-29Merge PR #8763: Adapt coq_makefile to handle coqpp-based macro files.Enrico Tassi
2018-10-26Add record names to multiple records error messageTej Chajed
2018-10-26Correctly report non-projection fields in recordsTej Chajed
2018-10-23Fixing #8794 (anomaly with abbreviation involving both term and binders).Hugo Herbelin
2018-10-21Adding a regression test for bug #8785 (missing univ constraints registration).Hugo Herbelin
2018-10-19Porting the test-suite to coqpp.Pierre-Marie Pédrot
2018-10-19Fix #8755: Uncaught exception Ltac_plugin.Taccoerce.CannotCoerceTo.Pierre-Marie Pédrot
2018-10-16Merge PR #8059: Simplify code for [Definition := Eval ...]Matthieu Sozeau
2018-10-16[test-suite] Update csdp cacheVincent Laporte
2018-10-15Correct some spelling errorsBenjamin Barenblat
2018-10-11Merge PR #8594: Miscellaneous refinements and cleaning of module printingEmilio Jesus Gallego Arias
2018-10-11[dune] [test-suite] Support for running the test suite with Dune.Emilio Jesus Gallego Arias
2018-10-11Merge PR #186: [RFC] Coqlib cleanupPierre-Marie Pédrot
2018-10-11[test-suite] Use the right OCAMLPATH separator on Windows.Emilio Jesus Gallego Arias
2018-10-10Miscellaneous refinements/cleaning of module printing.Hugo Herbelin
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-10[test-suite] Don't reset `OCAMLPATH`, but append to it.Emilio Jesus Gallego Arias
2018-10-10[test-suite] rename a fileVincent Laporte
2018-10-10Merge PR #6218: Fix #5197, handling of algebraic universesPierre-Marie Pédrot
2018-10-10Merge PR #8602: [test-suite] Use ocamlfind to locate Coq libraries in unit te...Enrico Tassi
2018-10-10Merge PR #8679: [test suite] Compile test cases, instead of only loading themEnrico Tassi
2018-10-09[default.nix] Add install dir to OCAMLPATH before running the test-suiteVincent Laporte
2018-10-09[test-suite] use “-async-proofs-cache force” when compilingVincent Laporte
2018-10-09[test-suite] Use ocamlfind to locate Coq libraries in unit tests.Emilio Jesus Gallego Arias
2018-10-09[test-suite] compile (rather than load) test casesVincent Laporte
2018-10-09[test-suite] ensure file names are valid module namesVincent Laporte
2018-10-09Simplify code for [Definition := Eval ...]Gaëtan Gilbert
2018-10-09Fix nativenorm when an evar is in the wrong place.Gaëtan Gilbert
2018-10-09Refactoring of Micromega code using a Simplex linear solverFrédéric Besson
2018-10-08Fixes #8672 (ill-formed pattern substitution in notation with "let").Hugo Herbelin
2018-10-08Fix #5197, handling of algebraic universesMatthieu Sozeau
2018-10-08Merge PR #8630: Some cleaning in the test suiteEnrico Tassi
2018-10-08Merge PR #8554: Fixes #8553: regression of tactic "change" under binders.Pierre-Marie Pédrot
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-10-04Merge PR #7361: Towards selecting "best" unification failure among severalPierre-Marie Pédrot
2018-10-04Test-suite: avoid explicit references to “Top”Vincent Laporte
2018-10-04test-suite: cleaningVincent Laporte
2018-10-04test-suite: rename a few filesVincent Laporte
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2018-10-03Merge PR #8634: (For v8.9 and master) Remove -compat 8.6 and document the com...Théo Zimmermann
2018-10-02Move the compat-update-process to right after branchingJason Gross
2018-10-02Update the -compat flagsJason Gross
2018-10-02Update compat notations to be compat 8.7Jason Gross
2018-10-02Revert #6651: Use r.(p) syntax to print primitive projectionsMaxime Dénès
2018-10-02Merge PR #7522: [ocaml] Update required OCaml version to 4.05.0Pierre-Marie Pédrot
2018-10-01Merge PR #7634: Extend combined scheme to Schemes in TypeMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 15:56:00 +0000