aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* romega: discard constructor D_mono (shorter trace + fix a bug)Gravatar Pierre Letouzey2017-05-22
* Merge PR#474: A fix for #5390 (a useful error on used introduction names was ...Gravatar Maxime Dénès2017-05-20
|\
* | Re-adding explicit dependency of misc universe test into all_stdlib.v.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
|\ \ \ \ \ \
| | | | | * | FIx bug #5300: uncaught exception in "Print Assumptions".Gravatar Cyprien Mangin2017-05-03
* | | | | | | Merge PR#541: Fixing "decide equality" bug #5449Gravatar Maxime Dénès2017-05-03
|\ \ \ \ \ \ \ | |_|_|_|_|_|/ |/| | | | | |
| | * | | | | Type@{_} should not produce a flexible algebraic universe.Gravatar Gaetan Gilbert2017-05-03
| | * | | | | Allow flexible anonymous universes in instances and sorts.Gravatar Gaetan Gilbert2017-05-03
* | | | | | | Merge PR#411: Mention template polymorphism in the documentation.Gravatar Maxime Dénès2017-05-03
|\ \ \ \ \ \ \ | |_|/ / / / / |/| | | | | |
| | | | | | * Merge PR#597: Fixing #5487 (v8.5 regression on ltac-matching expressions with...Gravatar Maxime Dénès2017-05-02
| | | | | | |\
| | | | | | * \ Merge PR#589: remove unneeded -emacs flag in coq-prog-args in test-suite filesGravatar Maxime Dénès2017-05-02
| | | | | | |\ \
| | | | | | * | | Fixing Set Rewriting Schemes bugs introduced in v8.5.Gravatar Hugo Herbelin2017-05-01
| | | | | | | * | remove unneeded -emacs flag to coq-prog-argsGravatar Paul Steckler2017-05-01
| | | | | | | | * Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).Gravatar Hugo Herbelin2017-05-01
| | | | | | | | * Really fixing #2602 which was wrongly working because of #5487 hiding the cause.Gravatar Hugo Herbelin2017-05-01
| | | | | | | |/ | | | | | | |/|
* | | | | | | | Fix bug #5501: Universe polymorphism breaks proof involving auto.Gravatar Pierre-Marie Pédrot2017-04-30
| | * | | | | | Fixing "decide equality"'s bug #5449.Gravatar Hugo Herbelin2017-04-30
| |/ / / / / / |/| | | | | |
| | | | | * | Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)."Gravatar Maxime Dénès2017-04-28
| | | | | |/
| | | | | * Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).Gravatar Hugo Herbelin2017-04-28
* | | | | | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Gravatar Maxime Dénès2017-04-28
|\ \ \ \ \ \
| | | | | | * Test for bug #5193: Uncaught exception Class_tactics.Search.ReachedLimitEx.Gravatar Pierre-Marie Pédrot2017-04-27
| | | | | * | Test surgical use of beta-iota in the type of variables coming fromGravatar Hugo Herbelin2017-04-27
| |_|_|_|/ / |/| | | | |
* | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-04-27
|\ \ \ \ \ \ | | |_|_|_|/ | |/| | | |
| | | | | * Add transparent_abstract tacticGravatar Jason Gross2017-04-25
| |_|_|_|/ |/| | | |
* | | | | Merge PR#574: Fix bug #5476: Ltac has an inconsistent view of hypotheses.Gravatar Maxime Dénès2017-04-24
|\ \ \ \ \
* \ \ \ \ \ Merge PR#565: Remove VernacErrorGravatar Maxime Dénès2017-04-24
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge branch v8.6 into trunkGravatar Hugo Herbelin2017-04-22
|\ \ \ \ \ \ \
| | * | | | | | Remove VernacErrorGravatar Gaetan Gilbert2017-04-21
| |/ / / / / / |/| | | | | |
| | | * | | | Fix bug #5377: @? patterns broken.Gravatar Pierre-Marie Pédrot2017-04-20
| | |/ / / / | |/| | | |
| | * | | | Fix bug #5476: Ltac has an inconsistent view of hypotheses.Gravatar Pierre-Marie Pédrot2017-04-19
| |/ / / / |/| | | |
| * | | | Merge PR#538: Correction of bug #4306Gravatar Maxime Dénès2017-04-19
| |\ \ \ \
* | | | | | Add a test for bug #5321: clearbody breaks typing of goal.Gravatar Pierre-Marie Pédrot2017-04-17