aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
* Merge PR#498: Bignums as a separate opam packageGravatar Maxime Dénès2017-06-14
|\
* \ Merge PR#385: Equality of sigma typesGravatar Maxime Dénès2017-06-13
|\ \
* \ \ Merge PR#757: Better sectioning on travis log printing in test-suiteGravatar Maxime Dénès2017-06-13
|\ \ \
| | | * BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-06-13
| |_|/ |/| |
* | | Merge PR#709: Bytecode compilation apart from 'make world', againGravatar Maxime Dénès2017-06-12
|\ \ \
* | | | Add support for "-bypass-API" argument of "coq_makefile"Gravatar Matej Košík2017-06-12
* | | | make test-suite/save-logs.sh usable also on old MacOS XGravatar Maxime Denes2017-06-12
| | * | Fix Travis sectioningGravatar Jason Gross2017-06-10
| | * | Better sectioning on travis log printing in test-suiteGravatar Jason Gross2017-06-09
| |/ / |/| |
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\ \ \
* \ \ \ Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...Gravatar Maxime Dénès2017-06-06
|\ \ \ \
* \ \ \ \ Merge PR#600: Some factorizations of ltac interpretation functions between ss...Gravatar Maxime Dénès2017-06-06
|\ \ \ \ \
* | | | | | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* | | | | | Merge PR#691: [travis] Add OSX test-suite checking.Gravatar Maxime Dénès2017-06-02
|\ \ \ \ \ \
| | | | * \ \ Merge PR#705: Fix bug #5019 (looping zify on dependent types)Gravatar Maxime Dénès2017-06-02
| | | | |\ \ \
* | | | | \ \ \ Merge PR#647: [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Maxime Dénès2017-06-02
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR#711: [gitlab] Artifact test suite logs on failure.Gravatar Maxime Dénès2017-06-02
|\ \ \ \ \ \ \ \ \
| | | * | | | | | | Test-suite: do not test native compiler if disabled by configure.Gravatar Maxime Dénès2017-06-01
| | | | | | | | * | test-suite/coq-makefile: we do not build byte file by default anymoreGravatar Pierre Letouzey2017-06-01
* | | | | | | | | | Merge PR#449: make specialize smarter (bug 5370).Gravatar Maxime Dénès2017-06-01
|\ \ \ \ \ \ \ \ \ \
| | | * | | | | | | | [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-06-01
| | | | | | | * | | | Merge PR#631: Fix bug #5255Gravatar Maxime Dénès2017-06-01
| | | | | | | |\ \ \ \
| | | | * | | | | | | | Fix coq_makefile uninstall target under OSX.Gravatar Maxime Dénès2017-06-01
| | | |/ / / / / / / /
* | | | | | | | | | | Merge PR#694: Fixing #5523 (missing support for complex constructions in recu...Gravatar Maxime Dénès2017-06-01
|\ \ \ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / / / |/| | | | | | | | | |
| | | | | | | | * | | Fix bug #5019 (looping zify on dependent types)Gravatar Jason Gross2017-06-01
| | | | | | | | * | | Add opened bug 5019Gravatar Jason Gross2017-06-01
| | | | | | * | | | | Merge PR#710: Add test-suite checks for coqchk with constraintsGravatar Maxime Dénès2017-06-01
| | | | | | |\ \ \ \ \ | | | | | | | |_|/ / / | | | | | | |/| | | |
* | | | | | | | | | | Merge PR#704: Fix empty parentheses display in test-suiteGravatar Maxime Dénès2017-06-01
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR#701: [readlink -f] doesn't work on OSXGravatar Maxime Dénès2017-05-31
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | * | | | | | | | [travis] print failing test suite logs on failureGravatar Gaëtan Gilbert2017-05-31
| | | | | | | | * | | | | Merge PR#560: Reinstate fixpoint refolding in [cbn], deactivated by mistake (...Gravatar Maxime Dénès2017-05-31
| | | | | | | | |\ \ \ \ \
| | | | * | | | | | | | | | Tests for new specialize feature + CHANGES.Gravatar Pierre Courtieu2017-05-31
| | | | | |_|_|_|_|_|_|/ / | | | | |/| | | | | | | |
| | | | | | | | * | | | | Merge PR#699: Fix bug 5550: "typeclasses eauto with" does not work with secti...Gravatar Maxime Dénès2017-05-31
| | | | | | | | |\ \ \ \ \
| | | | | | * | | | | | | | Factorizing interp_gen through a function interpreting glob_constr.Gravatar Hugo Herbelin2017-05-31
| | | | | |/ / / / / / / / | | | | |/| | | | | | | |
| | | | | | * | | | | | | More precise on preventing clash between bound vars name and hidden impargs.Gravatar Hugo Herbelin2017-05-31
| | | | | | * | | | | | | Fixing #5233 (missing implicit arguments for recursive records).Gravatar Hugo Herbelin2017-05-31
| | | | | | * | | | | | | Fixing a failure to interpret some local implicit arguments in Inductive.Gravatar Hugo Herbelin2017-05-31
| | | | | |/ / / / / / / | | | | |/| | | | | | |
| | | * | | | | | | | | Fixing #5523 (missing support for complex constructions in recursive notations).Gravatar Hugo Herbelin2017-05-31
| | | * | | | | | | | | Fixing a too lax constraint for finding recursive binder part of a notation.Gravatar Hugo Herbelin2017-05-31
| | | |/ / / / / / / /
| | | | * / / / / / / [gitlab] Artifact test suite logs on failure.Gravatar Gaëtan Gilbert2017-05-30
| | | |/ / / / / / /
| | | | | | | * / / Add test-suite checks for coqchk with constraintsGravatar Jason Gross2017-05-30
| | | | | |_|/ / / | | | | |/| | | |
| | * | / | | | | Fix empty parentheses display in test-suiteGravatar Jason Gross2017-05-30
| | |/ / / / / /
| | | * | | | | Merge PR#693: A subtle bug in tclWITHHOLES.Gravatar Maxime Dénès2017-05-30
| | | |\ \ \ \ \
| * | | | | | | | [readlink -f] doesn't work on OSXGravatar Gaëtan Gilbert2017-05-30
| |/ / / / / / /
* | | | | | | | Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
* | | | | | | | Few tests for e-variants of assert, set, remember.Gravatar Hugo Herbelin2017-05-30
|/ / / / / / /
| | | * | | | Fix bug 5550: "typeclasses eauto with" does not work with section variables.Gravatar Théo Zimmermann2017-05-30
* | | | | | | Merge PR#687: Gitlab CIGravatar Maxime Dénès2017-05-29
|\ \ \ \ \ \ \
| | * | | | | | Omega: use "simpl" only on coefficents, not on atoms (fix #4132)Gravatar Pierre Letouzey2017-05-29
| | | |/ / / / | | |/| | | |