aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine/vernacular-commands.rst
AgeCommit message (Collapse)Author
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-08Properly document the local and global locality attributes.Théo Zimmermann
2021-01-25Remove the SearchHead commandJim Fehrle
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-11-26[attributes] [typing] Rename `typing` to `bypass_check`Emilio Jesus Gallego Arias
As discussed in the Coq meeting.
2020-11-26[attributes] [doc] Documentation review by Théo.Emilio Jesus Gallego Arias
Co-authored-by: <Théo Zimmermann <theo.zimmermann@inria.fr>
2020-11-26[vernac] Allow to control typing flags with attributes.Emilio Jesus Gallego Arias
The syntax is the one of boolean attributes, that is to say `#[typing($flag={yes,no}]` where `$flag` is one of `guarded`, `universes`, `positive`. We had to instrument the pretyper in a few places, it is interesting that it is doing so many checks.
2020-11-24Convert auto chapter to prodnJim Fehrle
2020-11-14Distinguish one_pattern and one_term nonterminalsJim Fehrle
2020-11-12Clarifying the role of Add ML Path vs -I (see #13344).Hugo Herbelin
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
The smallcaps rendering was inexistent in the PDF version and did not look good in the HTML version.
2020-11-05Various fixes.Théo Zimmermann
2020-10-24Convert misc chapters to prodnJim Fehrle
2020-10-20Add some missing smallcaps.Théo Zimmermann
2020-09-11[refman] Rename int to integerPierre Roux
2020-09-11[refman] Rename num to naturalPierre Roux
2020-08-25Convert ltac2 chapter to use prodn, update syntaxJim Fehrle
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-05-16Merge PR #8855: More search optionsEmilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: kyoDralliam
2020-05-15Document new Search features.Théo Zimmermann
2020-05-14Add some markers of origin.Théo Zimmermann
2020-05-14Reintroduce leftover parts; update index files; small fixes.Théo Zimmermann
2020-05-09Add a `with_strategy` tacticJason Gross
Useful for guarding calls to `unfold` or `cbv` to ensure that, e.g., `Opaque foo` doesn't break some automation which tries to unfold `foo`. We have some timeouts in the strategy success file. We should not run into issues, because we are not really testing how long these take. We could just as well use `Timeout 60` or longer, we just want to make sure the file dies more quickly rather than taking over 10^100 steps. Note that this tactic does not play well with `abstract`; I have a potentially controversial change that fixes this issue. One of the lines in the doc comes from https://github.com/coq/coq/pull/12129#issuecomment-619771556 Co-Authored-By: Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr> Co-Authored-By: Théo Zimmermann <theo.zimmermann@inria.fr> Co-Authored-By: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
2020-05-01Remove flags, options and tables from vernac chapter.Théo Zimmermann
2020-04-28Merge PR #11718: Convert syntax extensions chapter to prodnThéo Zimmermann
Ack-by: JasonGross Ack-by: Zimmi48 Ack-by: cpitclaudel
2020-04-26Convert syntax extensions chapter to prodnJim Fehrle
2020-04-23Merge PR #12034: Make cumulative sprop a typing flag, deprecate command ↵Pierre-Marie Pédrot
line -sprop-cumulative Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-04-21Document changed warnings and erros following #12038.Théo Zimmermann
2020-04-16Make cumulative sprop a typing flag, deprecate command line -sprop-cumulativeGaëtan Gilbert
2020-04-11Merge PR #11961: Convert vernac commands chapter to prodn, update syntaxThéo Zimmermann
Ack-by: Zimmi48 Ack-by: cpitclaudel
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
2020-04-07Fix documentation of Print Libraries following #10476.Théo Zimmermann
2020-03-29Merge PR #11944: Remove SearchAbout command, deprecated in 8.5Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-28Document change of behavior of Fail in 8.11.Théo Zimmermann
2020-03-25Convert Gallina Extensions to use prodnJim Fehrle
2020-03-19Interpret the Export modifier of Set and Unset as an attribute.Théo Zimmermann
Unfortunately, we cannot go further and parse Export as a legacy attribute because this syntax conflicts with the Export command.
2020-03-19Document all the existing attributes.Théo Zimmermann
And fix documentation following the removal of the Template Check flag in #11546.
2020-03-18Add documentation for the export hint.Pierre-Marie Pédrot
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-01-10missing spaceOlivier Laurent
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
Update doc_grammar tool The grammar in the doc is generated semi-automatically with doc_grammar: - the grammar is automatically extracted from the mlg files - developer-prepared editing scripts *.mlg_edit modify the extracted grammar for clarity, simplicity and ordering of productions - chunks of the resulting grammar are automatically inserted into the rsts using instructions embedded in the rsts Running doc_grammar is currently a manual step. The grammar updates in the rst files have been manually reviewed.
2019-11-06Replace "option" in doc when it refers to a flagJim Fehrle
2019-09-19Fix #10420 Add dependent evar mapping info to outputJim Fehrle
2019-09-03Add missing index for From ... Require ...Théo Zimmermann
2019-08-16Universe Checking instead of Universes CheckingSimonBoulier
2019-08-16Add documentation for typing flags.SimonBoulier
2019-07-25Remove deprecated `Backtrack` commandMaxime Dénès
It has been deprecated since 8.4. The documentation was incorrect since at least 8.5 (the last two arguments were ignored). `Backtrack m n p` was a synonym for `BackTo m` We also move `BackTo` handling to coqtop, since it is not meant to be part of the document.
2019-05-23Suggestions from review.Théo Zimmermann
Co-authored-by: Jason Gross <jgross@mit.edu>
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 10:08:55 +0000