aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-13Fix Equation's ci scriptMatthieu Sozeau
2019-12-13Use ~strict argument consistently in push_context/push_context_set intfsMatthieu Sozeau
One should generally push contexts with ~strict:true when the context is a monomorphic one (all univs > Set) except for template polymorphic inductives (>= Prop) and ~strict:false for universe polymorphic ones (>= Set). Includes fixes from Gaëtan's and Emilio's reviews
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-12Fix #11195 and add other improvements: try loading .vio (and not just .vo) ↵charguer
if the .vos file is empty, rename -quick to -vio, dump empty .vos when producing .vio, dump empty .vos and .vok files when producing .vo from .vio.
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-10[library] [cleanup] Remove code duplication.Emilio Jesus Gallego Arias
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-08When printing term together with its type, use info that term is in context.Hugo Herbelin
This governs the printing of the explicitation of implicit arguments and the removal of coercions. E.g., "Check coe foo." where coe is a coercion with codomain B will show: foo : B instead of coe foo : B
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-06Make the string argument of `time` print correctlyJason Gross
Fixes #10971
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-06additional statements on flat_mapOlivier Laurent
2019-12-06additional statements on map and ForallOlivier Laurent
2019-12-06integration of statements for nthOlivier Laurent
2019-12-06add elt_eq_unitOlivier Laurent
2019-12-06integration of statements for Exists and ForallOlivier Laurent
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 21:40:44 +0000