aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2020-03-03[loadpath] Rework and simplify ML loadpath handlingEmilio Jesus Gallego Arias
This PR refactors the handling of ML loadpaths to get it closer to what (as of 2020) the standard OCaml toolchain (ocamlfind, dune) does. This is motivated as I am leaning toward letting the standard OCaml machinery handle OCaml includes; this has several benefits [for example plugins become regular OCaml libs] It will also help in improving dependency handling in plugin dynload. The main change is that "recursive" ML loadpaths are no longer supported, so Coq's `-I` option becomes closer to OCaml's semantics. We still allow `-Q` to extend the OCaml path recursively, but this may become deprecated in the future if we decide to install the ML parts of plugins in the standard OCaml location. Due to this `Loadpath` still hooks into `Mltop`, but other than that `.v` location handling is actually very close to become fully independent of Coq [thus it can be used in other tools such coqdep, the build system, etc...] In terms of vernaculars the changes are: - The `Add Rec ML Path` command has been removed, - The `Add Loadpath "foo".` has been removed. We now require that the form with the explicit prefix `Add Loadpath "foo" as Prefix.` is used. We did modify `fake_ide` as not to add a directory with the empty `Prefix`, which was not used. This exposed some bugs in the implementation of the document model, which relied on having an initial sentence; we have workarounded them just by adding a dummy one in the two relevant cases.
2020-02-29Merge PR #11701: Fix #11696: link from refman to stdlib doc is dead.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2020-02-28Merge PR #10008: CoqIDE: Fix not escaping coqtop arguments when compilingHugo Herbelin
Ack-by: ejgallego Ack-by: gares Ack-by: herbelin
2020-02-28Merge PR #11423: Convert Vernacular section of gallina chapter to use prodnThéo Zimmermann
Ack-by: SkySkimmer Ack-by: Zimmi48
2020-02-28Convert Gallina Vernac to use prodnJim Fehrle
2020-02-28Adding change logHugo Herbelin
2020-02-27Merge PR #11650: Set Printing ParensEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-27Fix #11696: link from refman to stdlib doc is dead.Théo Zimmermann
2020-02-26Addr 'attr' directive for attributesJim Fehrle
2020-02-26Fix changelog for https://github.com/coq/coq/pull/11686Maxime Dénès
2020-02-26Consolidate int63-related notationsMaxime Dénès
We avoid redundant notations for the same concepts and make sure notations do not break Ltac parsing for users of these libraries.
2020-02-25Merge PR #11663: Remove unqualified universe attributes.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-24Add OPTREF and INSERTALL editing operationsJim Fehrle
Show effect of edits to edited nt in PRINT Add cmdv:: info to prodnCommands Supporting code globally replaces a given "substring" in productions with another. (Substring over doc_symbols, not over characters.)
2020-02-24Generate prodnCommands file that compares commands in the grammar toJim Fehrle
those in the rsts.
2020-02-24Allow multiple indexed names on a single .. cmd::, etc.Jim Fehrle
2020-02-24Make it clear how to import Ltac2Clément Pit-Claudel
2020-02-24added sphinx docAbhishek Anand (optiplex7010@home)
2020-02-24added changelogAbhishek Anand (optiplex7010@home)
2020-02-23Merge PR #11120: Refactoring code for application printing + fixing #11091 ↵Emilio Jesus Gallego Arias
(inconsistencies in parsing/printing notations to partial applications) Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: jfehrle
2020-02-23Merge PR #11637: Update copyright in refman to year 2020.Clément Pit-Claudel
Reviewed-by: jfehrle
2020-02-23Remove unqualified universe attributes.Théo Zimmermann
They were already deprecated in two major releases.
2020-02-23Documenting inheritance of implicit arguments and scopes in notations.Hugo Herbelin
2020-02-23Addressing a changelog comment from Théo Zimmermann.Hugo Herbelin
2020-02-23Update ↵Hugo Herbelin
doc/changelog/03-notations/11120-master+refactoring-application-printing.rst Thanks Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2020-02-23Apply and generalize suggestions from Théo.Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2020-02-22Adding a changelog item.Hugo Herbelin
2020-02-21Merge PR #11590: Fixes #9741: only printing notations do not uselessly ↵Emilio Jesus Gallego Arias
reserve parsing keywords Reviewed-by: ejgallego
2020-02-21Merge PR #11261: Use implicit types for printing (granting wish #10366).Emilio Jesus Gallego Arias
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ejgallego
2020-02-21Adding changelog for #11590, fixing #9741.Hugo Herbelin
2020-02-21Merge PR #11617: [init] Add `-boot` option to avoid binding `Coq.` prefix.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: herbelin
2020-02-20Merge PR #10832: Addressing #6082 and #7766: warning when overriding ↵Emilio Jesus Gallego Arias
notation format + new notion of format associated to a given interpretation Ack-by: maximedenes
2020-02-20[init] Add `-boot` option to avoid binding `Coq.` prefix.Emilio Jesus Gallego Arias
This is useful when we want to have finer control of the location of files in the bootstrap process, for example when building using Dune. Also, this makes options consistent with what `coqdep` already uses for bootstrap. The main use case for `-boot` is to replace the hardcoded `add_load_path (coqlib () / theories)` with `-R dir Coq`, where dir is controlled by the build system. In particular, we use `-R . Coq` as we `cd` into the directory the package is, so without boot we'd have to hardcode the `theories` path in Dune itself. which seems less robust. Notably after this change the only part of the build that uses `coqlib` is the micromega solver, but that can be tweaked so if coqlib is not set it will use the one in the path. IMO not having to set "coqlib" is a good property if we want a more compositional setup.
2020-02-21Merge PR #11329: Fixing #11114: anomaly with Extraction Implicit on records.Kazuhiko Sakaguchi
Reviewed-by: pi8027
2020-02-20Merge PR #11616: [coqdep] Tweak changelog after recent PRs.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2020-02-20Adding changelog.Hugo Herbelin
2020-02-19Update copyright in refman to year 2020.Théo Zimmermann
2020-02-19Merge PR #11302: Add --fuzz, --real, --user to timing scriptsEmilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: jfehrle
2020-02-19Merge PR #11600: New syntax [Inductive Acc A R | x : Prop := ...]Emilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: maximedenes Reviewed-by: ppedrot
2020-02-19Adding change log for #10832.Hugo Herbelin
2020-02-19Short allusion in refman on the existence of a generic and specific format.Hugo Herbelin
2020-02-19Addressing #6082 and #7766 (overriding format of notation).Hugo Herbelin
We do two changes: - We distinguish between a notion of format generically attached to notations and a new notion of format attached to interpreted notations. "Reserved Notation" attaches a format generically. "Notation" attaches the format specifically to the given interpretation, and additionally, attaches it generically if it is the first time the notation is defined. - We warn before overriding an explicitly reserved generic format, or a specific format.
2020-02-18Merge PR #11530: Fixes custom entries precedence bugs (#11331 part)Pierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-02-18Merge PR #11529: [build] Consolidate stdlib's .v files under a single directory.Théo Zimmermann
Reviewed-by: Zimmi48
2020-02-18Updating reference manual and adding a change log entry.Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2020-02-17Merge PR #11350: stdlib List: add [remove'] and [count_occ'] that use [filter]Hugo Herbelin
Reviewed-by: anton-trunov
2020-02-17[coqdep] Tweak changelog after recent PRs.Emilio Jesus Gallego Arias
2020-02-17Merge PR #11614: Show apostrophes and backticks in HTML doc, too.Théo Zimmermann
Reviewed-by: Zimmi48
2020-02-17Merge PR #11589: [coqdep] Remove support for `-c` ocamldep replacement.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2020-02-17New syntax [Inductive Acc A R | x : Prop := ...]Gaëtan Gilbert
to control uniform parameters. This replaces the attribute.
2020-02-17Revert "Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)"Gaëtan Gilbert
This reverts commit bc2c1836ba4c878903288060bcb66a0ef1aaced6.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 15:37:25 +0000