aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* 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
| | * Fixing an extra bug with pattern_of_constr.Gravatar Hugo Herbelin2017-05-19
| |/ |/|
| * A fix for #5390 (a useful error on used introduction names was masked).Gravatar Hugo Herbelin2017-05-17
* | Merge PR#633: An extension of EXTEND and notations to make standard parsing t...Gravatar Maxime Dénès2017-05-17
|\ \ | |/ |/|
* | Merge PR#457: Adding an even more compact goal hyps mode.Gravatar Maxime Dénès2017-05-17
|\ \
* \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-05-17
|\ \ \
* \ \ \ Merge PR#620: Reorganization of the layout for miscellaneous testsGravatar Maxime Dénès2017-05-17
|\ \ \ \
| | | | * Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND.Gravatar Hugo Herbelin2017-05-16
| |_|_|/ |/| | |
| | | * Simplified compaction criterion + tests.Gravatar Pierre Courtieu2017-05-16
| | * | Fixing bug #5222 (anomaly with "`pat" in the presence of scope delimiters).Gravatar Hugo Herbelin2017-05-16
| | * | Fixing a bug with nested "as" clauses in "match".Gravatar Hugo Herbelin2017-05-16
* | | | Merge PR#594: An example showing the benefit of EconstrGravatar Maxime Dénès2017-05-11
|\ \ \ \
* \ \ \ \ Merge PR#373: A refined solution to the beta-iota discrepancies between 8.4 a...Gravatar Maxime Dénès2017-05-11
|\ \ \ \ \
* \ \ \ \ \ Merge PR#201: Transparent abstractGravatar Maxime Dénès2017-05-11
|\ \ \ \ \ \
| | | | * | | Moving code for miscellaneous tests to specific files.Gravatar Hugo Herbelin2017-05-10
| | | | * | | A more regular naming of variables in test-suite Makefile.Gravatar Hugo Herbelin2017-05-10
| | | | * | | Adding tests for testing exit status and #use"include".Gravatar Hugo Herbelin2017-05-10
| | | | * | | Cleaning old untested not any more interesting testing files.Gravatar Hugo Herbelin2017-05-10
| |_|_|/ / / |/| | | | |
* | | | | | Merge PR#558: Adding a fold_glob_constr_with_binders combinatorGravatar Maxime Dénès2017-05-05
|\ \ \ \ \ \
| | | | * | | Adding a test-suite pattern-unification example that Econstr fixed.Gravatar Hugo Herbelin2017-05-05
| |_|_|/ / / |/| | | | |
* | | | | | Merge PR#544: Anonymous universesGravatar Maxime Dénès2017-05-05
|\ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 09:13:58 +0000