aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-12-13[micromega] Enable ocamlformat.Emilio Jesus Gallego Arias
2019-12-13Merge PR #11259: [make] Rename Makefile to Makefile.make and INSTALL to ↵Théo Zimmermann
INSTALL.md Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: gares Ack-by: jfehrle
2019-12-13Merge PR #11257: [dev] [ocaml] Add ocamlformat configuration.Théo Zimmermann
Reviewed-by: Zimmi48
2019-12-13Add ocamlformat dependency to Nix fileMaxime Dénès
2019-12-13Merge PR #11283: Split up stdlib install command (too long)Maxime Dénès
Reviewed-by: maximedenes
2019-12-13[build] Allow the selection of build system using an env var.Emilio Jesus Gallego Arias
This is undocumented on purpose by now. Suggested by Gaëtan Gilbert
2019-12-13[doc] [INSTALL] split make-based install instructions to its own file.Emilio Jesus Gallego Arias
2019-12-13[doc] [INSTALL] Port INSTALL to markdown format.Emilio Jesus Gallego Arias
2019-12-13[make] Rename Makefile to Makefile.makeEmilio Jesus Gallego Arias
Picked from #8729. This should help preserve the history better when we split.
2019-12-13[fmt] [dune] Add ocamlformat configuration.Emilio Jesus Gallego Arias
For now we don't enable it in any source file, neither on dune files. `lint-repository` has been updated so it will check `dune build @fmt` returns 0.
2019-12-13[ci] [docker] Install ocamlformat in docker images.Emilio Jesus Gallego Arias
2019-12-13Split up stdlib install command (too long)Gaëtan Gilbert
2019-12-13Merge PR #10657: restrict minimization to set to flexiblesMaxime Dénès
Reviewed-by: mattam82
2019-12-13Merge PR #11281: [vm] Untabify the VM C code.Maxime Dénès
Reviewed-by: maximedenes
2019-12-12Merge PR #11278: Clean libobject stuffGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: maximedenes
2019-12-12restrict minimization to set to flexiblesGaëtan Gilbert
Split from #10331 Fix part of #8196 Replaces #9343
2019-12-12[vm] Untabify the VM C code.Emilio Jesus Gallego Arias
This is a follow up of #11010 ; I've realized that for example in #11123 a large part of the patch is detabification as indeed the files are mixed in tabs/space style so developers are forced to do the cleanup each time they work on them. Command used: ``` for i in `find . -name '*.c' -or -name '*.h'; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done ``` Checked empty diff with `git diff --ignore-all-space`
2019-12-12Merge PR #11264: Type safe summary & libobject implementationEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-12-12Merge PR #11276: Fixing #10750: "Print Visibility" raises Not_found on ↵Emilio Jesus Gallego Arias
only-printing notations Ack-by: cpitclaudel Reviewed-by: ejgallego
2019-12-11Remove the unused add_leaves Libobject primitive.Pierre-Marie Pédrot
2019-12-11Remove the reliance of ring objects on the named part.Pierre-Marie Pédrot
This was just dead code.
2019-12-11Merge PR #11201: remove *.vos and *.vok file in "make clean"Enrico Tassi
Reviewed-by: gares
2019-12-11Merge PR #11262: [hashset] Don't use deprecated Obj.truncatePierre-Marie Pédrot
Reviewed-by: ppedrot
2019-12-11Merge PR #11271: Fixing #9893. "Specialize with" would not support hyps type ↵Pierre-Marie Pédrot
containing letins. Reviewed-by: ppedrot
2019-12-10Fixing #10750 (anomaly of "Print Visibility" on only-printing notations).Hugo Herbelin
2019-12-10Merge PR #10202: Slightly more robust manual implicit argumentsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-12-10Merge PR #11269: Several cleanups and factorization in scheme declarationsEmilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Reviewed-by: ejgallego
2019-12-10Fixing #9893 (Letins not supported in the specialized hypothesis).Pierre Courtieu
2019-12-10Side-effect free wrapper around already declared schemes.Pierre-Marie Pédrot
Some calls are actually guarded by a check that the scheme is already in the cache. There is no reason to generate dummy side-effects in that case.
2019-12-10Make explicit that users should not observe return values of scheme functions.Pierre-Marie Pédrot
2019-12-10Simplify internal flags in scheme declarations.Pierre-Marie Pédrot
2019-12-10Merge PR #11268: dune: Add byte mode for coqchk and coqide (fix dune-dbg for ↵Emilio Jesus Gallego Arias
dune 2) Reviewed-by: ejgallego
2019-12-09dune: Add byte mode for coqchk and coqide (fix dune-dbg for dune 2)Gaëtan Gilbert
dune-dbg depends on coqchk.bc and coqide_main.bc, and apparently they now need explicit modes to be produced.
2019-12-09Type-safe implementation of libobjects.Pierre-Marie Pédrot
Same justification as the change in implementation of Summary.
2019-12-09Simplify the implementation of Summary by specifying the type of ML-MODULES.Pierre-Marie Pédrot
No need to deploy an existential type machinery when we already know this type in advance.
2019-12-09Type-safe implementation of summary state.Pierre-Marie Pédrot
For historical reasons we were wrapping the data stored in the summary objects with dynamic type casts. There is no reason to do so since we have a proper Dyn API. Furthermore, this had a small runtime cost when we knew that it was never going to fail.
2019-12-09Merge PR #11255: Fix #11254: "coqtop --version" working even in the middle ↵Emilio Jesus Gallego Arias
of an installation process Ack-by: Zimmi48 Reviewed-by: ejgallego
2019-12-09Fixes #11254 (not requiring coqlib to be set to report about coqtop version).Hugo Herbelin
2019-12-09Merge PR #10829: Section.t is never emptyPierre-Marie Pédrot
Ack-by: ejgallego Reviewed-by: ppedrot
2019-12-09Merge PR #11234: [ide] Don't use -linkall for the GUI app.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-12-09[hashset] Don't use deprecated Obj.truncateEmilio Jesus Gallego Arias
We follow the solution used upstream https://github.com/ocaml/ocaml/pull/2279 Fixes half of #10602
2019-12-09Merge PR #11256: [configure] [dune] Fix configure under Dune in 32bit builds.Théo Zimmermann
Reviewed-by: Zimmi48
2019-12-07Section.t is never emptyGaëtan Gilbert
This approach using `type t = { sec_prev: t option; sec_... }` makes it easy to update sections using the record update syntax, but impossible to statically ensure that an operation only affects the current section. We may instead consider using `type t = section * section list` which needs some boilerplate to update.
2019-12-07[configure] [dune] Fix configure under Dune in 32bit builds.Emilio Jesus Gallego Arias
`dev/header.c` is not registered as a dependency, so the configure step under dune fails in 32bit builds. Note we don't detect the problem due to dubious code in configure ignoring stderr messages on process calls.
2019-12-07Merge PR #11141: Moving the diversity of constr printers to a label styleEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego
2019-12-06Adding documentation in printer.mliHugo Herbelin
2019-12-06Adding overlay for Quickchick PR#145.Hugo Herbelin
2019-12-06Moving the diversity of constr printers to a label style.Hugo Herbelin
This allows to give access to all printing options (e.g. a scope or being-in-context) to every printer w/o increasing the numbers of functions.
2019-12-06Merge PR #11127: Added theorem Nat.bezout_comm.Hugo Herbelin
Ack-by: Zimmi48 Ack-by: herbelin
2019-12-06Merge PR #11232: Remove latex files that should be regenerated by makeThéo Zimmermann
Ack-by: Zimmi48
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 22:04:48 +0000