aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2020-05-18Update to 8.13.Théo Zimmermann
Part of this PR was automatically generated by running dev/doc/update-compat.py --master
2020-05-17Merge PR #11981: Ltac2: add notations for eval cbv in ... and other in place ↵Jason Gross
reductions Reviewed-by: JasonGross Ack-by: Zimmi48
2020-05-17Ltac2: add notations for eval cbv in ... and other in place reductionsMichael Soegtrop
2020-05-16Merge PR #12288: Prove that classical reals implement constructive reals.Michael Soegtrop
Reviewed-by: MSoegtropIMC Reviewed-by: Zimmi48
2020-05-16Merge PR #12326: Fix #11761: Functional Induction throws unrecoverable error.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-05-16Merge PR #12330: Add redirects for HTML pages that were moved.Clément Pit-Claudel
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-16Merge PR #12277: Checking validity of coqdoc file name (fixes #12265)Théo Zimmermann
Reviewed-by: Zimmi48 Ack-by: randomdross
2020-05-16Fix note on implicit arguments in doc of functional induction.Théo Zimmermann
2020-05-16Fix #11761: Functional Induction throws unrecoverable error.Pierre Courtieu
Error happened only when writing: functional induction f x y z. instead of functional induction (f x y z). Now the former is equivalent to the former: implicits must be omitted. Hence small source of incompatibility, but a more homogeneous behaviour.
2020-05-16Prove that classical reals implement constructive reals. Also move sums, min ↵Vincent Semeria
and max to CoRN. Update stdlib index Remove ConstructiveSum from the index Add changelog entry Make constructive reals experimental
2020-05-16Add redirects for HTML pages that were moved.Théo Zimmermann
2020-05-15Merge PR #12239: Split Gallina, Gallina ext and most of CIC chapters into ↵Clément Pit-Claudel
multiple pages. Reviewed-by: jfehrle
2020-05-15Changelog entries for #8855.Théo Zimmermann
2020-05-15Document new Search features.Théo Zimmermann
2020-05-15Move SSR's Search to a new plugin and deprecate it.Théo Zimmermann
2020-05-15Update docgram following #12122 and #12229.Théo Zimmermann
2020-05-15Merge PR #12323: Fixes #12322: anomaly when printing "fun" binders with ↵Emilio Jesus Gallego Arias
implicit types Reviewed-by: ejgallego
2020-05-15Merge PR #11948: Hexadecimal numeralsHugo Herbelin
Reviewed-by: JasonGross Ack-by: Zimmi48 Ack-by: herbelin
2020-05-15Merge PR #11755: [exn] [tactics] improve backtraces on monadic errorsPierre-Marie Pédrot
Ack-by: gares Ack-by: ppedrot
2020-05-15Fix typo.Théo Zimmermann
2020-05-15Merge PR #11992: do not re-export ListNotations from ProgramAnton Trunov
Reviewed-by: Zimmi48 Reviewed-by: anton-trunov Reviewed-by: ejgallego
2020-05-14Merge PR #12256: Move the static check of evaluability in unfold tactic to ↵Hugo Herbelin
runtime. Reviewed-by: herbelin
2020-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
Current backtraces for tactics leave a bit to desire, for example given the program: ```coq Lemma u n : n + 0 = n. rewrite plus_O_n. ``` the backtrace stops at: ``` Found no subterm matching "0 + ?M160" in the current goal. Called from file "proofs/proof.ml", line 381, characters 4-42 Called from file "tactics/pfedit.ml", line 102, characters 31-58 Called from file "plugins/ltac/g_ltac.mlg", line 378, characters 8-84 ``` Backtrace information `?info` is as of today optional in some tactics, such as `tclZERO`, it doesn't cost a lot however to reify backtrace information indeed in `tclZERO` and provide backtraces for all tactic errors. The cost should be small if we are not in debug mode. The backtrace for the failed rewrite is now: ``` Found no subterm matching "0 + ?M160" in the current goal. Raised at file "pretyping/unification.ml", line 1827, characters 14-73 Called from file "pretyping/unification.ml", line 1929, characters 17-53 Called from file "pretyping/unification.ml", line 1948, characters 22-72 Called from file "pretyping/unification.ml", line 2020, characters 14-56 Re-raised at file "pretyping/unification.ml", line 2021, characters 66-73 Called from file "proofs/clenv.ml", line 254, characters 12-58 Called from file "proofs/clenvtac.ml", line 95, characters 16-53 Called from file "engine/proofview.ml", line 1110, characters 40-46 Called from file "engine/proofview.ml", line 1115, characters 10-34 Re-raised at file "clib/exninfo.ml", line 82, characters 4-38 Called from file "proofs/proof.ml", line 381, characters 4-42 Called from file "tactics/pfedit.ml", line 102, characters 31-58 Called from file "plugins/ltac/g_ltac.mlg", line 378, characters 8-84 ``` which IMO is much better.
2020-05-14Merge PR #12296: Fixes #12234: wrong environment for Show ProofGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-14Add a changelog for 8.11.2.Pierre-Marie Pédrot
2020-05-14Fix title level and a build failure.Théo Zimmermann
2020-05-14Fix conflicts with latest master.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-14Adding changelog.Pierre-Marie Pédrot
2020-05-14Remove an outdated piece of documentation about limitations of unfold.Pierre-Marie Pédrot
2020-05-14Added change log.Hugo Herbelin
2020-05-14Refactoring of the first part of the reference manual.Théo Zimmermann
2020-05-14Preserve Implicit arguments file.Théo Zimmermann
2020-05-14Remove Canonical structures from Implicit arguments.Théo Zimmermann
2020-05-14Merge doc on Canonical structures from two origins.Théo Zimmermann
2020-05-14Move Canonical structures file into new location.Théo Zimmermann
2020-05-14Add Canonical structure declarations to Canonical structures file.Théo Zimmermann
2020-05-14Extract Canonical structures from Implicit arguments.Théo Zimmermann
2020-05-14Split Gallina extensions into multiple files.Théo Zimmermann
2020-05-14Split Gallina into multiple files.Théo Zimmermann
2020-05-14Split parts of CIC into multiple files.Théo Zimmermann
2020-05-14Create new file on Functions and Assumptions.Théo Zimmermann
2020-05-14Extract functions and assumptions.Théo Zimmermann
2020-05-14Merge definitions and type casts in same file.Théo Zimmermann
2020-05-14Create new file on Definitions.Théo Zimmermann
2020-05-14Extract Definitions from Gallina.Théo Zimmermann
2020-05-14Add type casts to new Definitions file.Théo Zimmermann
2020-05-14Extract type casts from Gallina.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:48:54 +0000