aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* Merge PR#691: [travis] Add OSX test-suite checking.Gravatar Maxime Dénès2017-06-02
|\
* \ Merge PR#647: [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Maxime Dénès2017-06-02
|\ \
* \ \ Merge PR#711: [gitlab] Artifact test suite logs on failure.Gravatar Maxime Dénès2017-06-02
|\ \ \
| | | * Test-suite: do not test native compiler if disabled by configure.Gravatar Maxime Dénès2017-06-01
* | | | Merge PR#449: make specialize smarter (bug 5370).Gravatar Maxime Dénès2017-06-01
|\ \ \ \
| | | * | [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-06-01
| | | | * Fix coq_makefile uninstall target under OSX.Gravatar Maxime Dénès2017-06-01
| | | |/
* | | | Merge PR#694: Fixing #5523 (missing support for complex constructions in recu...Gravatar Maxime Dénès2017-06-01
|\ \ \ \ | |_|_|/ |/| | |
* | | | Merge PR#704: Fix empty parentheses display in test-suiteGravatar Maxime Dénès2017-06-01
|\ \ \ \
* \ \ \ \ Merge PR#701: [readlink -f] doesn't work on OSXGravatar Maxime Dénès2017-05-31
|\ \ \ \ \
| | | | | * [travis] print failing test suite logs on failureGravatar Gaëtan Gilbert2017-05-31
| | | | * | Tests for new specialize feature + CHANGES.Gravatar Pierre Courtieu2017-05-31
| | | * | | Fixing #5523 (missing support for complex constructions in recursive notations).Gravatar Hugo Herbelin2017-05-31
| | | * | | Fixing a too lax constraint for finding recursive binder part of a notation.Gravatar Hugo Herbelin2017-05-31
| | | |/ /
| | | | * [gitlab] Artifact test suite logs on failure.Gravatar Gaëtan Gilbert2017-05-30
| | | |/
| | * / Fix empty parentheses display in test-suiteGravatar Jason Gross2017-05-30
| | |/
| * / [readlink -f] doesn't work on OSXGravatar Gaëtan Gilbert2017-05-30
| |/
* | Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
* | Few tests for e-variants of assert, set, remember.Gravatar Hugo Herbelin2017-05-30
|/
* Merge PR#687: Gitlab CIGravatar Maxime Dénès2017-05-29
|\
* \ Merge PR#689: Changes to make coq-makefile not failing on MacOS X.Gravatar Maxime Dénès2017-05-28
|\ \
* \ \ Merge PR#683: coq_makefile: build .cma for each .mlpackGravatar Maxime Dénès2017-05-28
|\ \ \
* \ \ \ Merge PR#684: Trunk+fix coq makefile test suite on nixosGravatar Maxime Dénès2017-05-28
|\ \ \ \
| | | | * Gitlab CIGravatar Gaëtan Gilbert2017-05-28
* | | | | Merge PR#680: add Show test with -emacs flag for trunkGravatar Maxime Dénès2017-05-28
|\ \ \ \ \ | |_|_|_|/ |/| | | |
| | | * | coq_makefile: build .cma for each .mlpackGravatar Enrico Tassi2017-05-27
| | * | | Add execution permission to test-suite file.Gravatar Théo Zimmermann2017-05-27
| | * | | Use specific shell for more robustness.Gravatar Théo Zimmermann2017-05-27
| | * | | Fix test-suite/coq-makefile on NixOS.Gravatar Théo Zimmermann2017-05-27
| |/ / / |/| | |
| | | * Changes to make coq-makefile not failing on MacOS X.Gravatar Hugo Herbelin2017-05-26
| |_|/ |/| |
* | | Merge PR#666: romega revisited : no more normalization trace, cleaned-up reso...Gravatar Maxime Dénès2017-05-26
|\ \ \ | |_|/ |/| |
| | * add Show test with -emacs flagGravatar Paul Steckler2017-05-25
| |/ |/|
* | Merge PR#637: Short cleaning of the interpretation path for constr_with_bindingsGravatar Maxime Dénès2017-05-25
|\ \
* \ \ Merge PR#406: coq makefile2Gravatar Maxime Dénès2017-05-25
|\ \ \
* \ \ \ Merge PR#642: Small cleanup on `close_proof` type.Gravatar Maxime Dénès2017-05-24
|\ \ \ \
* \ \ \ \ Merge PR#650: Fixing an extra bug with pattern_of_constrGravatar Maxime Dénès2017-05-24
|\ \ \ \ \
| | | * | | add the only targetGravatar Enrico Tassi2017-05-23
| | | * | | coq_makefile: don't quote extra arguments (-arg)Gravatar Enrico Tassi2017-05-23
| | | * | | test suite for coq_makefile2Gravatar Enrico Tassi2017-05-23
| | | * | | test suite for coq_makefileGravatar Enrico Tassi2017-05-23
| |_|/ / / |/| | | |
* | | | | Merge PR#661: Added a test for #4765 (an example of printing abbreviation wit...Gravatar Maxime Dénès2017-05-23
|\ \ \ \ \
* \ \ \ \ \ Merge PR#657: [test-suite] Add tests for goal printing.Gravatar Maxime Dénès2017-05-23
|\ \ \ \ \ \
| | | | * | | [vernac] Remove `Save.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
| |_|_|/ / / |/| | | | |
| | | | | * romega: discard constructor D_mono (shorter trace + fix a bug)Gravatar Pierre Letouzey2017-05-22
| |_|_|_|/ |/| | | |
| | | | * Using type classes in the interpretation of "specialize" and "contradiction".Gravatar Hugo Herbelin2017-05-22
| |_|_|/ |/| | |
| | * | Added a test for #4765 (an example of printing abbreviation with binders).Gravatar Hugo Herbelin2017-05-20
| |/ / |/| |
* | | Merge PR#474: A fix for #5390 (a useful error on used introduction names was ...Gravatar Maxime Dénès2017-05-20
|\ \ \
| | * | [test-suite] Add tests for goal printing.Gravatar Emilio Jesus Gallego Arias2017-05-20
| |/ / |/| |
* | | Re-adding explicit dependency of misc universe test into all_stdlib.v.Gravatar Hugo Herbelin2017-05-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 00:51:54 +0000