aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Merge branch 'v8.5' into trunkGravatar Maxime Dénès2016-07-04
|\
| * test-suite: test checking of libraries checksum.Gravatar Maxime Dénès2016-07-04
* | Adding test for #4811.Gravatar Hugo Herbelin2016-07-02
| * Fixing #4882 (anomaly with Declare Implicit Tactic on hole of type with evars).Gravatar Hugo Herbelin2016-07-01
* | Fixing #4865 (deciding on which arguments to recompute scopes was not robust).Gravatar Hugo Herbelin2016-06-29
* | Univs: Fix bug #4726Gravatar Matthieu Sozeau2016-06-29
* | Fix issues in test-suite revealed by warnings.Gravatar Maxime Dénès2016-06-29
* | Adding a test-suite for the only printing flag.Gravatar Pierre-Marie Pédrot2016-06-28
| * Univs: allowing notations to take univ instancesGravatar Matthieu Sozeau2016-06-27
| * Forbidding silently dropped universes instances inGravatar Matthieu Sozeau2016-06-27
* | Shrink Proofs/Obligations by default and deprecateGravatar Matthieu Sozeau2016-06-27
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\|
* | Patterns in binders: printing testsGravatar Arnaud Spiwack2016-06-27
* | Patterns in binders: functional testsGravatar Arnaud Spiwack2016-06-27
* | Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
| * More on f9695eb4b, 827663982 on resolving #4782, #4813 (typing "with" clause).Gravatar Hugo Herbelin2016-06-27
* | Fixing #4854 (regression introduced in 4d25b224 in relation with #4592).Gravatar Hugo Herbelin2016-06-24
* | Test-suite fix to 1744e37 (injection in context).Gravatar Hugo Herbelin2016-06-18
* | Adding an "as" clause to specialize.Gravatar Hugo Herbelin2016-06-18
* | Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
* | Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
* | par: like all: but in parallelGravatar Enrico Tassi2016-06-17
* | proof mode: print unification constraintsGravatar Matthieu Sozeau2016-06-16
* | Tentative fix of test-suite file to avoid loopGravatar Matthieu Sozeau2016-06-16
* | Cleanup and refactoringGravatar Matthieu Sozeau2016-06-16
* | Revise syntax of Hint CutGravatar Matthieu Sozeau2016-06-16
* | Example given at DeepSpec workshopGravatar Matthieu Sozeau2016-06-16
* | Purely refactoring and code/API cleanup.Gravatar Matthieu Sozeau2016-06-16
* | eauto: fix test-suite fileGravatar Matthieu Sozeau2016-06-16
* | bteauto: a Proofview.tactic for multiple goalsGravatar Matthieu Sozeau2016-06-16
* | Fix iterative deepening strategy failing too earlyGravatar Matthieu Sozeau2016-06-16
* | Implement limited proof search and iterative deepening.Gravatar Matthieu Sozeau2016-06-16
* | Typeclasses eauto based on new proof engine,Gravatar Matthieu Sozeau2016-06-16
* | Refine 9cc95f5, unification of Let-In's, bug #3929Gravatar Matthieu Sozeau2016-06-16
* | Not taking arguments given by name or position into account whenGravatar Hugo Herbelin2016-06-16
* | Merge 'pr/191' into trunkGravatar Enrico Tassi2016-06-16
|\ \
* \ \ Merge branch 'pr/146' into trunkGravatar Enrico Tassi2016-06-16
|\ \ \
* | | | Fix test-suite for opened bug #4813.Gravatar Pierre-Marie Pédrot2016-06-15
| * | | Merge branch 'pr/146' into trunkGravatar Enrico Tassi2016-06-15
|/| | |
| * | | ssrmatching: simple test for Ltac APIGravatar Enrico Tassi2016-06-15
* | | | fix test-suite/ide Makefile (stupid typo)Gravatar Enrico Tassi2016-06-15
|/ / /
| | * Merge branch 'bug4450' into v8.5Gravatar Matthieu Sozeau2016-06-14
| | |\
| | * \ Merge branch 'bug4725' into v8.5Gravatar Matthieu Sozeau2016-06-14
| | |\ \
| | * | | Admitted: fix #4818 return initial stmt and univsGravatar Matthieu Sozeau2016-06-14
* | | | | test-suiet: run fake_id as before pr/173 was mergedGravatar Enrico Tassi2016-06-14
* | | | | Merge remote-tracking branch 'origin/pr/173' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \ \ \
| | * | | | Ident selectors cannot be used inside an Ltac expression.Gravatar Cyprien Mangin2016-06-14
| | * | | | Goal selectors are now tacticals and can be used as such.Gravatar Cyprien Mangin2016-06-14
| | * | | | Remove the need for brackets in goal selectors.Gravatar Cyprien Mangin2016-06-14
| | * | | | Add test-suite file for goal selectors.Gravatar Cyprien Mangin2016-06-14
| |/ / / / |/| | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 17:42:27 +0000