aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-05-29Configuration: always giving a value to configdir and datadir.Hugo Herbelin
2017-05-29More structure and more code factorization in building defaultHugo Herbelin
2017-05-29Unifying the layout of installation directories.Hugo Herbelin
2017-05-29Unified terminology in configure.ml/coq_config.ml: arch_win32 -> arch_is_win32.Hugo Herbelin
2017-05-29Mini-renaming in configure.ml to avoid switching back and forth fromHugo Herbelin
2017-05-29Dead code (xdg_config_dirs).Hugo Herbelin
2017-05-28Merge PR#675: [coqlib] Deprecate redundant Coqlib functions.Maxime Dénès
2017-05-28Merge PR#683: coq_makefile: build .cma for each .mlpackMaxime Dénès
2017-05-28Merge PR#684: Trunk+fix coq makefile test suite on nixosMaxime Dénès
2017-05-28Merge PR#681: Fix votour for safe strings & warningsMaxime Dénès
2017-05-28Merge PR#680: add Show test with -emacs flag for trunkMaxime Dénès
2017-05-28Merge PR#676: Primitive Ltac definitions for first and solveMaxime Dénès
2017-05-28Merge PR#658: [coqdoc] Add keywords in bug 2884.Maxime Dénès
2017-05-27[coqlib] Deprecate redundant Coqlib functions.Emilio Jesus Gallego Arias
2017-05-27coq_makefile: build .cma for each .mlpackEnrico Tassi
2017-05-27Documenting the existence of first and solve as Ltac definitions.Pierre-Marie Pédrot
2017-05-27Exporting a few primitive tacticals as named Ltac definitions.Pierre-Marie Pédrot
2017-05-27Merge PR#686: [travis] temporary UniMath overlayMaxime Dénès
2017-05-27[travis] temporary UniMath overlayMaxime Dénès
2017-05-27Add execution permission to test-suite file.Théo Zimmermann
2017-05-27Use specific shell for more robustness.Théo Zimmermann
2017-05-27Fix test-suite/coq-makefile on NixOS.Théo Zimmermann
2017-05-26Merge pull request #7 from SkySkimmer/checker+fix_votourEmilio Jesús Gallego Arias
2017-05-26[checker] [votour] resolve warning 52 fragile constant patternGaëtan Gilbert
2017-05-26Merge PR#666: romega revisited : no more normalization trace, cleaned-up reso...Maxime Dénès
2017-05-26Merge PR#655: Extra functions exported in EConstrMaxime Dénès
2017-05-26[checker] Add bin/votour to the coqocaml target.Emilio Jesus Gallego Arias
2017-05-26[votour] Fix/disable warnings.Emilio Jesus Gallego Arias
2017-05-26[votour] Fix build with -safe-string (bug 5553)Emilio Jesus Gallego Arias
2017-05-25add Show test with -emacs flagPaul Steckler
2017-05-25Merge PR#645: [stm] Tweak debug options.Maxime Dénès
2017-05-25Merge PR#637: Short cleaning of the interpretation path for constr_with_bindingsMaxime Dénès
2017-05-25Merge PR#608: Allow Ltac2 as a pluginMaxime Dénès
2017-05-25Merge PR#481: [option] Remove support for non-synchronous options.Maxime Dénès
2017-05-25Merge PR#406: coq makefile2Maxime Dénès
2017-05-25Merge PR#402: Uniform attribute handling in interfacesMaxime Dénès
2017-05-25[location] [travis] Add overlays for located_switchEmilio Jesus Gallego Arias
2017-05-24[location] Fix warnings.Emilio Jesus Gallego Arias
2017-05-24[location] Renaming "CAst.ast" to "CAst.t"Matej Košík
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-24ROmega: division-aware ReflOmegaCore, allowing trace without termsPierre Letouzey
2017-05-24[option] Remove support for non-synchronous options.Emilio Jesus Gallego Arias
2017-05-24coq_makefile: use -include rather than includeEnrico Tassi
2017-05-24Merge PR#642: Small cleanup on `close_proof` type.Maxime Dénès
2017-05-24Merge PR#650: Fixing an extra bug with pattern_of_constrMaxime Dénès
2017-05-24Merge PR#671: unification.mli: Fix a spelling typo in a commentMaxime Dénès
2017-05-23unification.mli: Fix a spelling typo in a commentJason Gross
2017-05-23add the only targetEnrico Tassi
2017-05-23travis: coq_makefile needs the tipa packageEnrico Tassi
2017-05-23overlay for UniMathEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:14:35 +0000