aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Cleanup: removal of constr_of_global.Gravatar Matthieu Sozeau2017-05-29
* Merge PR#512: [cleanup] Unify all calls to the error function.Gravatar Maxime Dénès2017-05-29
|\
* \ Merge PR#678: [coqlib] Move `Coqlib` to `library/`.Gravatar Maxime Dénès2017-05-28
|\ \
* \ \ Merge PR#689: Changes to make coq-makefile not failing on MacOS X.Gravatar Maxime Dénès2017-05-28
|\ \ \
* \ \ \ Merge PR#675: [coqlib] Deprecate redundant Coqlib functions.Gravatar Maxime Dénès2017-05-28
|\ \ \ \
* \ \ \ \ Merge PR#683: coq_makefile: build .cma for each .mlpackGravatar Maxime Dénès2017-05-28
|\ \ \ \ \
* \ \ \ \ \ Merge PR#684: Trunk+fix coq makefile test suite on nixosGravatar Maxime Dénès2017-05-28
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR#681: Fix votour for safe strings & warningsGravatar Maxime Dénès2017-05-28
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR#680: add Show test with -emacs flag for trunkGravatar Maxime Dénès2017-05-28
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR#676: Primitive Ltac definitions for first and solveGravatar Maxime Dénès2017-05-28
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR#658: [coqdoc] Add keywords in bug 2884.Gravatar Maxime Dénès2017-05-28
|\ \ \ \ \ \ \ \ \ \
| | | | | | | | | | * [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
| |_|_|_|_|_|_|_|_|/ |/| | | | | | | | |
| | | | | | | | | * [coqlib] Move `Coqlib` to `library/`.Gravatar Emilio Jesus Gallego Arias2017-05-27
| | | | | | | | |/ | | | | | | | |/|
| | | | | | | * | [coqlib] Deprecate redundant Coqlib functions.Gravatar Emilio Jesus Gallego Arias2017-05-27
| |_|_|_|_|_|/ / |/| | | | | | |
| | | | | | * | coq_makefile: build .cma for each .mlpackGravatar Enrico Tassi2017-05-27
| | * | | | | | Documenting the existence of first and solve as Ltac definitions.Gravatar Pierre-Marie Pédrot2017-05-27
| | * | | | | | Exporting a few primitive tacticals as named Ltac definitions.Gravatar Pierre-Marie Pédrot2017-05-27
| |/ / / / / / |/| | | | | |
* | | | | | | Merge PR#686: [travis] temporary UniMath overlayGravatar Maxime Dénès2017-05-27
|\ \ \ \ \ \ \
| * | | | | | | [travis] temporary UniMath overlayGravatar Maxime Dénès2017-05-27
|/ / / / / / /
| | | | * | | Add execution permission to test-suite file.Gravatar Théo Zimmermann2017-05-27
| | | | * | | Use specific shell for more robustness.Gravatar Théo Zimmermann2017-05-27
| | | | * | | Fix test-suite/coq-makefile on NixOS.Gravatar Théo Zimmermann2017-05-27
| |_|_|/ / / |/| | | | |
| | | | | * Changes to make coq-makefile not failing on MacOS X.Gravatar Hugo Herbelin2017-05-26
| |_|_|_|/ |/| | | |
| | | * | Merge pull request #7 from SkySkimmer/checker+fix_votourGravatar Emilio Jesús Gallego Arias2017-05-26
| | | |\ \
| | | | * | [checker] [votour] resolve warning 52 fragile constant patternGravatar Gaëtan Gilbert2017-05-26
| | | |/ /
* | | | | Merge PR#666: romega revisited : no more normalization trace, cleaned-up reso...Gravatar Maxime Dénès2017-05-26
|\ \ \ \ \
* \ \ \ \ \ Merge PR#655: Extra functions exported in EConstrGravatar Maxime Dénès2017-05-26
|\ \ \ \ \ \ | |_|_|_|_|/ |/| | | | |
| | | | | * [checker] Add bin/votour to the coqocaml target.Gravatar Emilio Jesus Gallego Arias2017-05-26
| | | | | * [votour] Fix/disable warnings.Gravatar Emilio Jesus Gallego Arias2017-05-26
| | | | | * [votour] Fix build with -safe-string (bug 5553)Gravatar Emilio Jesus Gallego Arias2017-05-26
| |_|_|_|/ |/| | | |
| | | | * add Show test with -emacs flagGravatar Paul Steckler2017-05-25
| |_|_|/ |/| | |
* | | | Merge PR#645: [stm] Tweak debug options.Gravatar Maxime Dénès2017-05-25
|\ \ \ \
* \ \ \ \ Merge PR#637: Short cleaning of the interpretation path for constr_with_bindingsGravatar Maxime Dénès2017-05-25
|\ \ \ \ \
* \ \ \ \ \ Merge PR#608: Allow Ltac2 as a pluginGravatar Maxime Dénès2017-05-25
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR#406: coq makefile2Gravatar Maxime Dénès2017-05-25
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR#402: Uniform attribute handling in interfacesGravatar Maxime Dénès2017-05-25
|\ \ \ \ \ \ \ \ \
| * | | | | | | | | [location] [travis] Add overlays for located_switchGravatar Emilio Jesus Gallego Arias2017-05-25
| * | | | | | | | | [location] Fix warnings.Gravatar Emilio Jesus Gallego Arias2017-05-24
| * | | | | | | | | [location] Renaming "CAst.ast" to "CAst.t"Gravatar Matej Košík2017-05-24
| * | | | | | | | | Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
| |\ \ \ \ \ \ \ \ \ | |/ / / / / / / / / |/| | | | | | | | |
| | | | | | | | * | ROmega: division-aware ReflOmegaCore, allowing trace without termsGravatar Pierre Letouzey2017-05-24
| | | * | | | | | | [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| | * | | | | | | | coq_makefile: use -include rather than includeGravatar Enrico Tassi2017-05-24
* | | | | | | | | | Merge PR#642: Small cleanup on `close_proof` type.Gravatar Maxime Dénès2017-05-24
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR#650: Fixing an extra bug with pattern_of_constrGravatar Maxime Dénès2017-05-24
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR#671: unification.mli: Fix a spelling typo in a commentGravatar Maxime Dénès2017-05-24
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|/ / / / / / / |/| | | | | | | | | | |
| * | | | | | | | | | | unification.mli: Fix a spelling typo in a commentGravatar Jason Gross2017-05-23
|/ / / / / / / / / / /
| | | | * | | | | | | add the only targetGravatar Enrico Tassi2017-05-23
| | | | * | | | | | | travis: coq_makefile needs the tipa packageGravatar Enrico Tassi2017-05-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 03:22:05 +0000