aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-10-02Handling VERNAC EXTEND in coqpp.Pierre-Marie Pédrot
2018-10-02Pass unnamed arguments to ML macros.Pierre-Marie Pédrot
This was imposing a bit of useless burden on the API for no good reason.
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-02Fix deprecation warnings.Pierre-Marie Pédrot
2018-10-01Docs: Missing backquoteJoachim Breitner
2018-10-02[dune] Install more files from `tools`.Emilio Jesus Gallego Arias
These are needed for example for the test suite.
2018-10-02[tools] Remove unused / obsolete files.Emilio Jesus Gallego Arias
TTBOMK we don't use any of these files since a long time.
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-01fix deprecation warningsYves Bertot
2018-10-01Merge PR #8501: [classes] Split large `new_instance` function up.Matthieu Sozeau
2018-10-01adapts to master on Oct. 1st 2018, but warnings remainYves Bertot
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-01Fix checker soundness bug with polymorphism capturing global univsGaëtan Gilbert
Followup for #8341. Not making a test as that's too difficult with our current infrastructure.
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-30[api] Cleanup `Decls`: remove unused function, move vernac helper.Emilio Jesus Gallego Arias
It seems these two functions don't belong there. We can remove one, and place the other actually next to whether their semantics are necessary. Note that indeed the whole `Decls` file seems a bit suspicious, why we do we register this information in a separate table instead of in the main ones in `Lib` ? At the suggestion of Gaëtan Gilbert we also remove unused function `is_instance`.
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 00:49:01 +0000