aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-12-23[flags] Move global time flag into an attribute.Emilio Jesus Gallego Arias
One less global flag.
2017-12-22Merge PR #6465: Gitlab touchupMaxime Dénès
2017-12-22Merge PR #6469: No universe constraints in Let definitionsMaxime Dénès
2017-12-22Merge PR #6318: Separate vernac controls and regular commands.Maxime Dénès
2017-12-22Merge PR #6484: Update README and CONTRIBUTING to mention the wiki and FAQ.Maxime Dénès
2017-12-22Merge PR #6485: Fix badges.Maxime Dénès
2017-12-22Merge PR #6445: [stm] [ide protocol] Allow to include several commands on query.Maxime Dénès
2017-12-22Merge PR #6222: Share computation of unifiable evarsMaxime Dénès
2017-12-21Fix badges.Théo Zimmermann
2017-12-21Update README and CONTRIBUTING to mention the wiki and FAQ.Théo Zimmermann
2017-12-21Merge PR #6474: Fix CI with parallel make (messed up dependencies)Maxime Dénès
2017-12-21Fix CI with parallel make (messed up dependencies)Gaëtan Gilbert
When invoking through Makefile we always rebuild dependencies. To skip dependencies, invoke ci-wrapper directly. We make Circle CI do this. In order to properly support invoking ci-wrapper directly we replace "make" in ci-common by a bash function which adds -j to the make invocation outside submakes. We also set TIMED in the ci-wrapper.
2017-12-20Separate vernac controls and regular commands.Maxime Dénès
Virtually all classifications of vernacular commands (the STM classifier, "filtered commands", "navigation commands", etc.) were broken in presence of control vernaculars like Time, Timeout, Fail. Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac Debug in CoqIDE. This change introduces a type separation between vernacular controls and vernacular commands, together with an "under_control" combinator.
2017-12-20Merge PR #6377: Removal of the FAQ LaTex document.Maxime Dénès
2017-12-20Merge PR #6470: Fix typo in the refman.Maxime Dénès
2017-12-20Merge PR #6449: Let definitions must not contain side-effects when reaching ↵Maxime Dénès
the kernel.
2017-12-20Merge PR #6468: Fix order of let-in representation comment.Maxime Dénès
2017-12-20Merge PR #6471: Fix ltacprof_abstract (I think because of #6411 parallel merge).Maxime Dénès
2017-12-20Merge PR #6234: Make the micromega extraction check a regular output test.Maxime Dénès
2017-12-19Fix ltacprof_abstract (I think because of #6411 parallel merge).Gaëtan Gilbert
2017-12-19Fix typo in the refman.Théo Zimmermann
2017-12-19Let definitions do not create new universe constraints.Pierre-Marie Pédrot
We force the upper layers to extrude the universe constraints before sending it to the kernel. This simplifies the suspicious handling of polymorphic constraints for section-local definitions.
2017-12-19Merge PR #6400: Circle CIMaxime Dénès
2017-12-19Specific type for section definition entries.Pierre-Marie Pédrot
This allows to statically ensure well-formedness properties.
2017-12-19Fix order of let-in representation comment.Jasper Hugunin
The comment had the type and value of the let-in swapped, which contradicted the listed types.
2017-12-18Gitlab: don't ./configure in documentation jobGaëtan Gilbert
The config/Makefile is carried over by artefacts.
2017-12-18Merge PR #6436: Fix #5368: Canonical structure unification fails.Maxime Dénès
2017-12-18Merge PR #6447: [make] More build fixes for static plugins and ocamlfind.Maxime Dénès
2017-12-18Merge PR #6284: Warning for absolute name masking (deprecated, should become ↵Maxime Dénès
an error)
2017-12-18Merge PR #6381: A version of [time] that works on constr evaluationMaxime Dénès
2017-12-18Merge PR #6406: Make [abstract] nodes show up in the Ltac profileMaxime Dénès
2017-12-18Merge PR #6380: Add tactics to reset and display the Ltac profileMaxime Dénès
2017-12-18Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in ↵Maxime Dénès
Extraction Language command
2017-12-18Merge PR #6305: Build with windows line endingsMaxime Dénès
2017-12-18Merge PR #6217: Do dependencies in 1 command per file class.Maxime Dénès
2017-12-18Removing the FAQ, which has been moved to the GitHub wiki for thisMatt Quinn
repository. Also removing FAQ-related build rules.
2017-12-18Merge PR #6453: [doc] Nit on the manual.Maxime Dénès
2017-12-18Merge PR #6411: Fix #5081 by more fine-grained LtacProf recordingMaxime Dénès
2017-12-18Merge PR #6419: [vernac] Split `command.ml` into separate files.Maxime Dénès
2017-12-18Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Maxime Dénès
2017-12-17[flags] Make program_mode a parameter for commands in vernac.Emilio Jesus Gallego Arias
This is useful as it allows to reflect program_mode behavior as an attribute.
2017-12-17[vernac] Split `command.ml` into separate files.Emilio Jesus Gallego Arias
Over the time, `Command` grew organically and it has become now one of the most complex files in the codebase; however, its functionality is well separated into 4 key components that have little to do with each other. We thus split the file, and also document the interfaces. Some parts of `Command` export tricky internals to use by other plugins, and it is common that plugin writers tend to get confused, so we are more explicit about these parts now. This patch depends on #6413.
2017-12-17[doc] Nit on the manual.Emilio Jesus Gallego Arias
`ssrnat` is mentioned, but it is not distributed with Coq.
2017-12-16Fix build fileJim
2017-12-16For bug 6249, Segmentation fault when building Coq on Windows 10.Jim
Enable builds on Windows by removing Windows-style endings where it impacts make. The fix in Makefile.build is a band-aid fix; maximedenes said he would remove the dependency on sed and awk here.
2017-12-16Let definitions must not contain side-effects when reaching the kernel.Pierre-Marie Pédrot
Let definitions have the same behaviour if they are ended with a Qed or a Defined command, i.e. they are treated as if they were transparent. Indeed, it doesn't make sense for them to be opaque as they are going to be expanded away at the end of the section. For an unknown reason, handling of side-effects in Let definitions considers them as if they were opaque, i.e. the effects are inlined in the definition. This discrepancy has bad consequences in the kernel, where one is forced to juggle with universe constraints generated by polymorphic Let definitions. As a first phase of cleaning, we simply enforce by typing that Let definitions should be purified before reaching the kernel. This has the intended side-effect to make side-effects persistent in Let definitions, as if they were indeed truly transparent.
2017-12-16[make] More build fixes for static plugins and ocamlfind.Emilio Jesus Gallego Arias
- In ocamlfind-based byte builds, link the VM statically as in native builds. This is the best way to get reliable, path-independent self-contained executables. - In `make install`, install the `.cmx` files for plugins too. To statically link Coq plugins in native mode, both the `.cmx` and `.o` files must be present.
2017-12-16[stm] [ide protocol] Allow to include several commands on query.Emilio Jesus Gallego Arias
This is a very useful feature for IDEs, as they can queue commands and display options in a single request. Change is backwards-compatible.
2017-12-15Overlay for unimath.Gaëtan Gilbert
2017-12-15Do dependencies in 1 command per file class.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 21:27:27 +0000