aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
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-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
2018-09-28Merge PR #262: A cleaning step in using heuristics for inference of the retur...Pierre-Marie Pédrot
2018-09-28Merge PR #8479: Fix #8478: Undeclared universe anomaly with sectionsPierre-Marie Pédrot
2018-09-27Possible abstractions over goal variables when inferring match return clause.Hugo Herbelin
2018-09-27Trying an abstracting dependencies heuristic for the match return clause even...Hugo Herbelin
2018-09-27Trying a no-inversion no-dependency heuristic for match return clause.Hugo Herbelin
2018-09-27Inference of return clause: giving uniformly priority to "small inversion".Hugo Herbelin
2018-09-27Unification failure: don't give preference to a "beyond capabilities" error.Hugo Herbelin
2018-09-27Scheme Equality: support for working in a context of Parameters.Hugo Herbelin
2018-09-27Fixing a typo in a comment.Hugo Herbelin
2018-09-27Fixing #4859 (anomaly with Scheme called on inductive type with indices).Hugo Herbelin
2018-09-27Fixing #4612 (anomaly with Scheme called on unsupported inductive type).Hugo Herbelin
2018-09-27Fix #8478: Undeclared universe anomaly with sectionsGaëtan Gilbert
2018-09-27Fixes #8553 (regression of tactic "change" under binders).Hugo Herbelin
2018-09-27Merge PR #8475: Centralize the reliance on abstract universe context internalsGaëtan Gilbert
2018-09-26[ocaml] Update required OCaml version to 4.05.0Emilio Jesus Gallego Arias
2018-09-26Merge PR #8504: Allow successive attributes #[foo] #[bar]Vincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 22:44:51 +0000