aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Expand)AuthorAge
* 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
* | Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
* | par: like all: but in parallelGravatar Enrico Tassi2016-06-17
* | 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
* | Merge 'pr/191' into trunkGravatar Enrico Tassi2016-06-16
|\ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 20:34:39 +0000