aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-10-02[ocaml] [lib] Remove some compatibility layers for OCaml < 4.03.0Emilio Jesus Gallego Arias
2018-10-02Merge PR #8572: [config] Miscellaneous cleaning of configuration variables.Pierre-Marie Pédrot
2018-10-02Merge PR #8612: Fix issue 8610 - Change important CI DOS batch files to CRLFThéo Zimmermann
2018-10-02Merge PR #8614: [dune] [doc] Some tweaks to doc + per user flags.Théo Zimmermann
2018-10-02[dune] [doc] Some tweaks to doc + per user flags.Emilio Jesus Gallego Arias
2018-10-02Merge PR #7522: [ocaml] Update required OCaml version to 4.05.0Pierre-Marie Pédrot
2018-10-02Merge PR #7823: [tactics] function to gather undef evars of the goalPierre-Marie Pédrot
2018-10-02Merge PR #8595: Replacing Refine.pr_constr by Termops.Internal.print_constr.Pierre-Marie Pédrot
2018-10-01Merge PR #8531: [ci] Add plugin-tutorial to CI.Gaëtan Gilbert
2018-10-01Merge PR #8565: Make coqpp handle OCaml locationsEmilio Jesus Gallego Arias
2018-10-01Print location in OCaml code output by coqpp.Pierre-Marie Pédrot
Fixes #8018.
2018-10-01Store locations of OCaml quotations in coqpp.Pierre-Marie Pédrot
2018-10-01Merge PR #7372: Four new lemmas for listsHugo Herbelin
2018-10-01Fix issue 8610 - Change important CI DOS batch files to CRLFMichael Soegtrop
2018-10-01[ci] Add plugin-tutorial to CI.Emilio Jesus Gallego Arias
This closes #7618.
2018-10-01Merge PR #8254: Inline the definition of CClosure.mk_clos_deep.Maxime Dénès
2018-10-01Merge PR #8577: Generalize type of compare_head_with functions, and use for ↵Pierre-Marie Pédrot
econstr
2018-10-01Merge PR #8575: Remove {Safe_typing,Global}.push_contextMaxime Dénès
2018-10-01Merge PR #8579: [dune] [merlin] Fix some usability issues.Maxime Dénès
2018-10-01Merge PR #7634: Extend combined scheme to Schemes in TypeMatthieu Sozeau
2018-10-01Merge PR #8177: Make the warning for non-imported hints compatible with ↵Matthieu Sozeau
internal backtracking
2018-10-01Merge PR #8501: [classes] Split large `new_instance` function up.Matthieu Sozeau
2018-10-01Merge PR #8608: [default.nix] Add odoc to the documentation build-inputsThéo Zimmermann
2018-10-01Merge PR #8606: [dune] [configure] Fix typo in default prefix setting.Théo Zimmermann
2018-10-01Merge PR #517: Some lemmas about dependent equalityPierre-Marie Pédrot
2018-10-01Merge PR #8301: Documentation for proof diffsThéo Zimmermann
2018-10-01Merge PR #8604: Fix issue 8603 Move Windows CI runs to folder C:/ciThéo Zimmermann
2018-10-01[default.nix] Add odoc to the documentation build-inputsVincent Laporte
2018-10-01[default.nix] Update the reference to nixpkgs; make it the defaultVincent Laporte
2018-10-01[config] Remove unused ML variables.Emilio Jesus Gallego Arias
These are unused and not likely to come back.
2018-10-01[envars] Small implementation cleanup for coqlib internals.Emilio Jesus Gallego Arias
2018-10-01[lib] [flags] Move coqlib handling out of `Flags`Emilio Jesus Gallego Arias
The relevant logic is already in `Envars`, so it makes sense to make it private and don't expose the low-level implementation of the logic.
2018-10-01[lib] [flags] Move private IDE functions to `ide`Emilio Jesus Gallego Arias
2018-10-01[nit] Qualify `Envars` use.Emilio Jesus Gallego Arias
This eases grep to implement a different location system.
2018-10-01[envars] Defer CAMLP5 location to configure.Emilio Jesus Gallego Arias
These functions are unused, and configure should suffice for this purpose.
2018-10-01[dune] [configure] Fix typo in default prefix setting.Emilio Jesus Gallego Arias
Fix silly typo that created havoc in developer out-of-the-box setups.
2018-09-30Fix issue 8603 Move Windows CI runs to folder C:/ciMichael Soegtrop
2018-09-30Merge PR #8599: Typo in top_printers.mlPierre-Marie Pédrot
2018-09-30Merge PR #8590: Functionalizing calls to the environment in HimsgPierre-Marie Pédrot
2018-09-30 Merge PR #8597: [dune] Enable warning 60 [unused local module]Théo Zimmermann
2018-09-30Typo in top_printers.ml.Hugo Herbelin
2018-09-29[classes] Split large `new_instance` function up.Emilio Jesus Gallego Arias
`Classes.new_instance` is one of the largest functions of the codebase; we split it up and reduce indentation. This will help further cleanups. This PR should introduce no code changes other than splitting the function up.
2018-09-29[dune] Enable warning 60 [unused local module]Emilio Jesus Gallego Arias
This corrects a discrepancy with the make-based system.
2018-09-29Merge PR #8588: [dune] Pack checker to avoid [odoc] problems + build doc for ↵Théo Zimmermann
plugins.
2018-09-29New lemmas for List.vSimon Marechal
* ext_in_map * map_ext_in_iff * firstn_skipn_comm * skipn_firstn_comm * skipn_O * skipn_nil * skipn_cons * skipn_none * skipn_all * skipn_all2 * skipn_app * seq_ap * skipn_app * skipn_length * firstn_skipn_rev * firstn_rev * skipn_rev * seq_app All proofs by Anton Trunov.
2018-09-29Replacing Refine.pr_constr by Termops.Internal.print_constr.Hugo Herbelin
2018-09-28Functionalizing calls to the environment in Himsg.Hugo Herbelin
This shall eventually allow to call Himsg at any point of the execution, independently of the exact current global environment.
2018-09-28[dune] Pack checker to avoid [odoc] problems + build doc for plugins.Emilio Jesus Gallego Arias
We also build documentation for plugins, for example Ltac_plugin is often used in other plugins.
2018-09-28Merge PR #262: A cleaning step in using heuristics for inference of the ↵Pierre-Marie Pédrot
return clause
2018-09-28Cleanup comparisons in econstr (compare_head_... users)Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 21:21:00 +0000