aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
...
| * | | | | Fix a bug in cumulativityGravatar Amin Timany2017-06-16
| * | | | | Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
| * | | | | Move (part of) tests from checker to successGravatar Amin Timany2017-06-16
| * | | | | Checker add test for non-trivial constraintsGravatar Amin Timany2017-06-16
| * | | | | Change the option to Set Inductive CumulativityGravatar Amin Timany2017-06-16
| * | | | | Correct coqchk reductionGravatar Amin Timany2017-06-16
| * | | | | Disable debug printingGravatar Amin Timany2017-06-16
| * | | | | Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
| * | | | | Fix bugsGravatar Amin Timany2017-06-16
|/ / / / /
| | | | * Merge PR#713: Bump year in headers.Gravatar Maxime Dénès2017-06-15
| | | | |\
| | | | * \ Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraintsGravatar Maxime Dénès2017-06-15
| | | | |\ \
| | | | * \ \ Merge PR#752: Adding a test case as requested in bug 5205.Gravatar Maxime Dénès2017-06-15
| | | | |\ \ \
| | | | * \ \ \ Merge PR#747: Fix Bug #5568, no dup notation warnings on repeated module importsGravatar Maxime Dénès2017-06-15
| | | | |\ \ \ \
* | | | | \ \ \ \ Merge PR#719: Constrexpr.Numeral without bigintGravatar Maxime Dénès2017-06-15
|\ \ \ \ \ \ \ \ \
| | | | * | | | | | plugins/ltac : avoid spurious .cmxs filesGravatar Pierre Letouzey2017-06-15
* | | | | | | | | | Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\ \ \ \ \ \ \ \ \ \
* | | | | | | | | | | Remove dependency on -compat flag in coq_makefile test suite.Gravatar Maxime Dénès2017-06-15
| |_|_|_|/ / / / / / |/| | | | | | | | |
* | | | | | | | | | Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Maxime Dénès2017-06-14
|\ \ \ \ \ \ \ \ \ \
| | | | | * | | | | | [typeclasses eauto] Fix bug #3943: non-termination in topologicalGravatar Matthieu Sozeau2017-06-14
* | | | | | | | | | | Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
| | | * | | | | | | | Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Gravatar Pierre Letouzey2017-06-14
| |_|/ / / / / / / / |/| | | | | | | | |
| | * | | | | | | | Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-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
| | | | | * | | | | | A stronger test that #use"include";; works well.Gravatar Hugo Herbelin2017-06-11
| |_|_|_|/ / / / / / |/| | | | | | | | |
| | * | | | | | | | Fix Travis sectioningGravatar Jason Gross2017-06-10
| | * | | | | | | | Better sectioning on travis log printing in test-suiteGravatar Jason Gross2017-06-09
| |/ / / / / / / / |/| | | | | | | |
| | | | | * | | | Fix Bug #5568, no dup notation warnings on repeated module importsGravatar Paul Steckler2017-06-09
| | | * | | | | | A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
| |_|/ / / / / / |/| | | | | | |
* | | | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\ \ \ \ \ \ \ \ | | |_|/ / / / / | |/| | | | | |
| | | | | * | | Adding a test case as requested in bug 5205.Gravatar Théo Zimmermann2017-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
|\ \ \ \ \ \ \ \
| | | | | | | * | Univs: fix bug #5365, generation of u+k <= v constraintsGravatar Matthieu Sozeau2017-06-05
* | | | | | | | | 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
| | | |/ / / / / / / / / /
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 06:08:02 +0000