aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Expand)AuthorAge
* Fix typeclasses eauto shelving.Gravatar Théo Zimmermann2016-11-30
* Revert more of a477dc for good measureGravatar Matthieu Sozeau2016-11-16
* Revert part of a477dc, disallow_shelvedGravatar Matthieu Sozeau2016-11-15
* Fix test-suite files relying on tcs bugsGravatar Matthieu Sozeau2016-11-03
* typeclasses eauto Implem/doc of shelving strategyGravatar Matthieu Sozeau2016-11-03
* Fix handling of only_classes at toplevelGravatar Matthieu Sozeau2016-11-03
* Test new syntax for hints and typeclass optionsGravatar Matthieu Sozeau2016-11-03
* Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
* Merge remote-tracking branch 'github/pr/321' into v8.6Gravatar Maxime Dénès2016-10-28
|\
* \ Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-24
|\ \
* | | Merge branch 'v8.5' into v8.6Gravatar Hugo Herbelin2016-10-24
| * | Fixing #3479 (parsing of "{" and "}" when a keyword starts with "{" or "}").Gravatar Hugo Herbelin2016-10-24
| | * sections/hints: prevent Not_found in get_type_ofGravatar Matthieu Sozeau2016-10-21
| |/ |/|
* | Merge PR #300 into v8.6Gravatar Pierre-Marie Pédrot2016-10-17
|\ \
* | | Example illustrating non-local inference of the default type of impossible br...Gravatar Hugo Herbelin2016-10-17
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
|\ \ \ | | |/ | |/|
| * | Fixing a collision about the meta-variable ".." in recursive notations.Gravatar Hugo Herbelin2016-10-12
* | | Reverting generalization and cleaning of the return clause inference in v8.6.Gravatar Hugo Herbelin2016-10-11
* | | Clean up type classes flags and update compat file.Gravatar Maxime Dénès2016-10-05
* | | fixing bug 4609: document an option governing the generation of equalitiesGravatar Yves Bertot2016-10-03
* | | More tests for tactic "subst".Gravatar Hugo Herbelin2016-10-02
| | * Move vector/list compat notations to their relevant filesGravatar Jason Gross2016-09-29
| |/ |/|
* | Argument : assert does fail if no arg is given (fix #4864)Gravatar Enrico Tassi2016-09-29
* | Typeclass backtracking example by J. LeivantGravatar Matthieu Sozeau2016-09-28
* | Merge remote-tracking branch 'github/pr/232' into v8.6Gravatar Maxime Dénès2016-09-28
|\ \
* | | Posssible abstractions over goal variables when inferring match return clause.Gravatar Hugo Herbelin2016-09-26
* | | Trying an abstracting dependencies heuristic for the match return clause even...Gravatar Hugo Herbelin2016-09-26
* | | Trying a no-inversion no-dependency heuristic for match return clause.Gravatar Hugo Herbelin2016-09-26
* | | Further "decide equality" tests on demand of Jason.Gravatar Hugo Herbelin2016-09-17
* | | Added a test file for contradiction.Gravatar Hugo Herbelin2016-09-15
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-14
|\ \ \ | | |/ | |/|
| * | Fixing test-suite after commit 43104a0b.Gravatar Pierre-Marie Pédrot2016-09-14
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-21
|\| |
| * | Fixing an anomaly in printing a unification error message.Gravatar Hugo Herbelin2016-08-20
* | | Merge remote-tracking branch 'origin/pr/246' into v8.6Gravatar Matthieu Sozeau2016-08-19
|\ \ \
* | | | Fixing a collision about the meta-variable ".." in recursive notations.Gravatar Hugo Herbelin2016-07-16
| * | | Add test for pi_eq_proofs.Gravatar Matthieu Sozeau2016-07-08
* | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-07
|\ \ \ \ | |/ / / |/| / / | |/ /
* | | Fixed bug #4622.Gravatar Matthieu Sozeau2016-07-06
* | | Disallow dependent case on prim records w/o etaGravatar Matthieu Sozeau2016-07-06
* | | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2016-07-04
|\ \ \
| | * | congruence: Restrict refreshing to SetGravatar Matthieu Sozeau2016-07-04
| | * | congruence/univs: properly refresh (fix #4609)Gravatar Matthieu Sozeau2016-07-04
| |/ /
| | * Goal selectors now use the keyword [only].Gravatar Cyprien Mangin2016-06-30
| |/ |/|
* | Adding a test-suite for the only printing flag.Gravatar Pierre-Marie Pédrot2016-06-28
| * Forbidding silently dropped universes instances inGravatar Matthieu Sozeau2016-06-27
* | Patterns in binders: functional testsGravatar Arnaud Spiwack2016-06-27
* | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 11:09:47 +0000