aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-03-27Split coqdoc section out of utility chapter (octopus merge).Théo Zimmermann
This octopus merge is meant to preserve the commit history / blame of both parts.
2020-03-27Move section on coqdoc to new location.Théo Zimmermann
2020-03-27Remove the part about coqdoc from the utilities chapter.Théo Zimmermann
(It was moved out onto a separate page.)
2020-03-27Prepare split of section about coqdoc.Théo Zimmermann
2020-03-26Merge PR #11929: Reintroduce a command that was actually used in another ↵Clément Pit-Claudel
one. Fix build of PDF manual. Reviewed-by: cpitclaudel
2020-03-26Reintroduce commands that were actually used. Fix build of PDF manual.Théo Zimmermann
2020-03-26Merge PR #11877: Removing deprecated destruct/remember syntax _eqn.Théo Zimmermann
Reviewed-by: Zimmi48
2020-03-26Change logHugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2020-03-26Merge PR #11920: Shrink refman-prelude files.Clément Pit-Claudel
Ack-by: SkySkimmer Reviewed-by: cpitclaudel
2020-03-26CIC is printed in all-caps.Théo Zimmermann
As CIC is really an acronym, it should be printed in all-caps.
2020-03-26Removing deprecated destruct syntax _eqn.Hugo Herbelin
2020-03-26Shrink refman-prelude files.Théo Zimmermann
2020-03-26Merge PR #11918: Fix #11845: anomaly when including partially applied functorPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-26Merge PR #11919: Remove outdated mention of -allow-sprop.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-26Remove outdated mention of -allow-sprop.Théo Zimmermann
2020-03-26Fix #11845: anomaly when including partially applied functorGaëtan Gilbert
2020-03-26Merge PR #11913: Doc_grammar: Update cmd:: and tacn:: constructs in .rstsThéo Zimmermann
Reviewed-by: Zimmi48
2020-03-26Merge PR #11832: [ocamlformat] Use doc-comments=before style.Théo Zimmermann
Reviewed-by: Zimmi48
2020-03-26Merge PR #11885: Sorting: Swap the names of Sorted_sort and LocallySorted_sortHugo Herbelin
Reviewed-by: herbelin
2020-03-26Merge PR #11891: Fix levels of `<=?` and `<?` in the stdlibHugo Herbelin
Reviewed-by: herbelin
2020-03-25Merge PR #11898: Switch opam file to makeEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-03-25[ocamlformat] Use doc-comments=before style.Emilio Jesus Gallego Arias
IMHO it is a bit more logical, WDYT?
2020-03-25Doc_grammar: Update cmd:: and tacn:: constructs in .rstsJim Fehrle
Remove unneeded source and output files Move all commands under command NT Add a lot of edits for commands and tactics
2020-03-25Merge PR #11705: Convert Gallina Extensions chapter to use prodnsThéo Zimmermann
Ack-by: Zimmi48
2020-03-25Convert Gallina Extensions to use prodnJim Fehrle
2020-03-25Merge PR #11785: [proof] consolidation of mutual definition declaration pathGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: herbelin Reviewed-by: ppedrot
2020-03-25Merge PR #11875: Fix deploy of refman following #11855.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: ejgallego
2020-03-25Add a specific opam file to build te docker imagePierre Roux
The Docker image coqorg/coq:dev is currently built using the OPAM file coq.opam. Since this file is used for develoment purpose, it would be better to use a more stable one for building the docker images. The OPAM option "--locked=docker" will then be used in the opam pin command when building the docker image to use the new coq.opam.docker file. The new file builds Coq using make, this is temporary and could be reverted to dune once it supports "-native-compiler yes".
2020-03-25[declare] make restrict_ucontext an optional parameter.Emilio Jesus Gallego Arias
The current API does just exist as a workaround for a bug.
2020-03-25[lemmas] Use direct-style for mutual lemma declaration.Emilio Jesus Gallego Arias
Steps towards unification with `DeclareDef` API.
2020-03-25[lemmas] Use direct-style for variable declaration.Emilio Jesus Gallego Arias
Steps towards unification with `DeclareDef` API.
2020-03-25[proof] [mutual] Factorize mutual per-entry informationEmilio Jesus Gallego Arias
We move `Recthm` to `DeclareDef` so it is shared by interactive and direct fixpoint declaration. This is the last step before unifying both paths.
2020-03-25[proof] [mutual] Factorize universe handling.Emilio Jesus Gallego Arias
Note that we had to introduce a `restrict_ucontext` parameter to be faithful to the implementation in obligations, however this looks like a bug.
2020-03-25[proof] [mutual] Factorize mutual body construction.Emilio Jesus Gallego Arias
2020-03-25[proof] [mutual] Factorize notation declaration.Emilio Jesus Gallego Arias
2020-03-25[proof] Factorize call info message in mutual declarationsEmilio Jesus Gallego Arias
2020-03-25[proof] Start of mutual definition save refactoring.Emilio Jesus Gallego Arias
First commit of a series that will unify (and enforce) the handling of mutual constants. We will split this in several commits as to easy debugging / bisect in case of problems. In this first commit, we move the actual declare logic to a common place.
2020-03-24Merge PR #11703: Making of NumTok an API for numeralPierre-Marie Pédrot
Reviewed-by: SkySkimmer Reviewed-by: ppedrot Reviewed-by: proux01
2020-03-24Merge PR #11772: [obligations] Don't allocate libobjects for obligation info.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-24Merge PR #11826: [proof] Deprecate unused tacmach functions.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-24Merge PR #11858: Rename Retypeops -> RelevanceopsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-24Fix world and watch targets of Makefile.dune now that doc has install rules.Théo Zimmermann
2020-03-24Fix deploy of refman following #11855.Théo Zimmermann
2020-03-24Merge PR #11892: [refman] Fix caching, which was broken by the addition of ↵Théo Zimmermann
coq_config Reviewed-by: Zimmi48
2020-03-23Merge PR #9607: [ci] add metacoqGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: ejgallego
2020-03-23[refman] Fix caching, which was broken by the addition of coq_configClément Pit-Claudel
2020-03-23Fix levels of `<=?` and `<?` in the stdlibJason Gross
They were defined at level 70, no associativity in all but three places, where they were instead declared at level 35. Fixes #11890
2020-03-23[ci] add metacoqMatthieu Sozeau
2020-03-23Sorting: Swap the names of Sorted_sort and LocallySorted_sortLysxia
2020-03-23Merge PR #11888: Fix broken links in prodn:: in docThéo Zimmermann
Reviewed-by: Zimmi48
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:27:18 +0000