aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2018-11-12Test case for #4771: Substitution of inline global reference in tactics is br...Maxime Dénès
2018-11-09Merge PR #8601: Move bound universe names to abstract contextsGaëtan Gilbert
2018-11-09Add a test for bug #8939.Pierre-Marie Pédrot
2018-11-09Use arrays of names instead of lists in abstract universe names.Pierre-Marie Pédrot
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-11-08Standardize handling of Automatic Introduction.Jasper Hugunin
2018-11-07Revert "Do not allow spliting in res_pf, this is reserved for pretyping"Enrico Tassi
2018-11-06Merge PR #8556: [ssr] use tclDISPATCH for IPatDispatch (fix #8544)Maxime Dénès
2018-11-05Merge PR #8515: Command driven attributesPierre-Marie Pédrot
2018-11-05Merge PR #8870: Pass native and VM flags to the kernel through environmentPierre-Marie Pédrot
2018-11-05Merge PR #8874: Fix #8873: coqchk on inductive with letin parameterPierre-Marie Pédrot
2018-11-05Merge PR #8882: Fix #8881: validate fails to use inductive equivalence in cas...Pierre-Marie Pédrot
2018-11-05Pass native and VM flags to the kernel through environmentMaxime Dénès
2018-11-03Merge PR #8877: Fix #8876: expected number of arguments for cumulative constr...Pierre-Marie Pédrot
2018-11-03Merge PR #8745: Fixes #3468: making tactic-in-term sensitive to interpretatio...Pierre-Marie Pédrot
2018-11-02Remove is_universe_polymorphism from printingGaëtan Gilbert
2018-11-02Remove incorrect is_universe_polymorphism from modinternGaëtan Gilbert
2018-11-02Make attributes more general to make defining #[universes(...)] easyGaëtan Gilbert
2018-11-02gitignore test-suite/misc/poly-capture-global-univs/src/evil.mlGaëtan Gilbert
2018-10-31Partial fix of #8706 (tactic-in-term sensitive to seemingly unrelated scopes).Hugo Herbelin
2018-10-31[ssr] better doc for the IPatDispatch ASTEnrico Tassi
2018-10-31test-suite entry for issue #8544Cyril Cohen
2018-10-31Merge PR #8759: Fix #8755: Uncaught exception Ltac_plugin.Taccoerce.CannotCoe...Hugo Herbelin
2018-10-31Fix #8881: validate fails to use inductive equivalence in case_infoGaëtan Gilbert
2018-10-31Fix #8876: expected number of arguments for cumulative constructorsGaëtan Gilbert
2018-10-31Fix #8873: coqchk on inductive with letin parameterGaëtan Gilbert
2018-10-31No need to require List in test-suite/success/Inductive.vGaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 19:13:00 +0000