aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2020-04-22Merge PR #11928: Remove probably useless doc/sphinx/coqdoc.css.Hugo Herbelin
2020-04-22Merge PR #12031: [stdlib] A library on cyclic permutations: CPermutationHugo Herbelin
Ack-by: Zimmi48 Ack-by: anton-trunov Reviewed-by: herbelin
2020-04-22Merge PR #12023: Adding a Declare ML Module in empty file Ltac.vEmilio Jesus Gallego Arias
Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: ppedrot
2020-04-21Change log for #12023Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2020-04-21Adding a Declare ML Module in empty file Ltac.v.Hugo Herbelin
Indeed, it would be intuitive that `Require Import Ltac` is an equivalent for Ltac of `Require Import Ltac2.Ltac2`. Also declaring the classic proof mode.
2020-04-21Document changed warnings and erros following #12038.Théo Zimmermann
2020-04-21Update common.edit_mlg and fullGrammar following #12038.Théo Zimmermann
2020-04-21Merge PR #12060: CoqIDE: Disable client-side decoration on WindowsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-21Merge PR #12116: Fixing #12045: missing normalization in conclusion of ↵Pierre-Marie Pédrot
custom induction scheme Reviewed-by: ppedrot
2020-04-21Merge PR #12014: [stdlib] Add properties of operations on vectorsHugo Herbelin
Reviewed-by: herbelin
2020-04-21Merge PR #11883: Fix #7812: autounfold's behavior depends on file namesHugo Herbelin
Reviewed-by: herbelin
2020-04-20Merge PR #12126: TIMEFMT: Display the output file nameGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-20Adding change log for PR #12026 (definitions in coqdoc link to themselves).Hugo Herbelin
2020-04-20TIMEFMT: Display the output file nameJason Gross
We now use `$@` rather than `$*` so that we display the output target rather than the stem of the rule. This is more consistent for rules that users add (where the pattern variable might be something insufficiently identifying), and also generalizes more nicely to mixing multiple compilers (we get a clear difference between producing OCaml files and producing .vo files, even if the filename is the same up to the suffix). The result is that it's easy to describe what the timing information of the build log records: each time comes with a label which is a file name, and the time is the time it takes to produce that file.
2020-04-20Remove coqremote stylesheets which were useless since the Sphinx migration.Théo Zimmermann
2020-04-20Remove probably useless doc/sphinx/coqdoc.css.Théo Zimmermann
2020-04-20Adding change log.Hugo Herbelin
2020-04-20Merge PR #12123: Don't create index entries for the name "_"Théo Zimmermann
Reviewed-by: cpitclaudel
2020-04-20Change log for PR #12045.Hugo Herbelin
2020-04-20Merge PR #12106: Coqide: Apply style scheme and language settings to the ↵Pierre-Marie Pédrot
three sourceview buffers. Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-04-19added changelog for PR 12044ilya
Update doc/changelog/10-standard-library/12044-issue-12015.rst Co-Authored-By: Jason Gross <jasongross9@gmail.com> Apply suggestions from code review
2020-04-19A library on cyclic permutations: CPermutationOlivier Laurent
(following the pattern of Permutation.v)
2020-04-19Don't create index entries for the name "_"Jim Fehrle
2020-04-19Merge PR #12033: Let coqdoc be informed by coq about binding variables ↵Lysxia
(incidentally fixes #7697) Reviewed-by: Lysxia
2020-04-19CoqIDE: Adding a short documentation on style/theme customization.Hugo Herbelin
2020-04-17Coqide: Apply style scheme and language to the three buffers.Hugo Herbelin
It was previously only applied to the script buffer.
2020-04-17Deprecate “omega”Vincent Laporte
2020-04-17ZArith: move lia hints to a dedicated moduleVincent Laporte
2020-04-17Merge PR #11963: NativeCompute Timing: Use real, not user timePierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-04-17Merge PR #11972: Fix require in sectionPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-04-16NativeCompute Timing: Use real, not user timeJason Gross
User time is unreliable for `native_compute`. Also output time spent in conversion to native code, just in case that is ever slow. Note that this also removes spurious newlines in the output. Fixes #11962
2020-04-16Merge PR #12070: Ignore -native-compiler option when disabledPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-04-16Merge PR #11861: [declare] [rewrite] Use high-level declare APIPierre-Marie Pédrot
Reviewed-by: SkySkimmer Ack-by: herbelin Reviewed-by: ppedrot
2020-04-16CoqIDE: Disable client-side decoration on WindowsAttila Gáspár
2020-04-15Adding change log for PR #12033 (hyperlinks on binders for coqdoc).Hugo Herbelin
2020-04-15[declare] Rename `Declare.t` to `Declare.Proof.t`Emilio Jesus Gallego Arias
This still needs API cleanup but we defer it to the moment we are ready to make the internals private.
2020-04-15[proof] Merge `Proof_global` into `Declare`Emilio Jesus Gallego Arias
We place creation and saving of interactive proofs in the same module; this will allow to make `proof_entry` private, improving invariants and control over clients, and to reduce the API [for example next commit will move abstract declaration into this module, removing the exported ad-hoc `build_constant_by_tactic`] Next step will be to unify all the common code in the interactive / non-interactive case; but we need to tweak the handling of obligations first.
2020-04-15[proof] Move proof_global functionality to Proof_global from PfeditEmilio Jesus Gallego Arias
This actually gets `Pfedit` out of the dependency picture [can be almost merged with `Proof` now, as it is what it manipulates] and would allow to reduce the exported low-level API from `Proof_global`, as `map_fold_proof` is not used anymore.
2020-04-15Ignore -native-compiler option when disabledPierre Roux
2020-04-14Merge PR #11957: [stdlib] update sigma-type notationsHugo Herbelin
Reviewed-by: JasonGross Ack-by: herbelin
2020-04-14Merge PR #12037: coqdoc: Report location of mismatched '[['Hugo Herbelin
Reviewed-by: herbelin
2020-04-13Fix #11783 Require in SectionGaëtan Gilbert
2020-04-13Update syntax of Import / Export in documentation.Théo Zimmermann
2020-04-13doc for partial importsGaë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-11add properties of operations on vectorsOlivier Laurent
2020-04-11Fix #7812Attila Gáspár
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
2020-04-10coqdoc: Report location of mismatched '[['Lysxia
2020-04-10Suppress the space after "#" when printing productionsJim Fehrle
to reflect lexer requirement for no space
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 21:11:39 +0000