aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
2019-10-22documentation fixesAntonio Nikishaev
document « Property » more documentation fixes [doc] destructed → destructured [doc] another le_minus→lt_1_r [doc] @jfehrle suggestions [doc] more minor fixes
2019-10-22Merge PR #10880: Allow to pass Ltac1 values to Ltac2 quotations.Jason Gross
Ack-by: SkySkimmer Reviewed-by: Zimmi48
2019-10-18Allow to pass Ltac1 values to Ltac2 quotations.Pierre-Marie Pédrot
This is the dual of #10344.
2019-10-16Define sphinx replacements for \SProp \Type etcGaëtan Gilbert
2019-10-15Merge PR #10854: Fix alphabetical ordering in contributors to 8.10.0.Clément Pit-Claudel
Ack-by: cpitclaudel Reviewed-by: jfehrle
2019-10-14Merge PR #10883: Doc update with mlg extension - fix #10855Jason Gross
Reviewed-by: JasonGross Reviewed-by: gares Ack-by: ppedrot
2019-10-14Merge PR #10811: Allow SProp default onPierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-10-13Doc update with mlg extension - fix #10855mcaci
2019-10-11Merge PR #10489: Fix output for "Printing Dependent Evars Line"Hugo Herbelin
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: hendriktews Reviewed-by: herbelin Ack-by: mattam82
2019-10-09Fix alphabetical ordering in the list of contributors to 8.10.Théo Zimmermann
Also remove Pierre Letouzey from the list because his contribution was the numeral notation feature which ended up being backported to 8.9, after the branching, but before the first beta release.
2019-10-06Merge PR #10834: Fix #10831: minor issues in documentation of Function.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-10-06Fix #10831: minor issues in documentation of Function.Théo Zimmermann
2019-10-068.10.0 release notes.Théo Zimmermann
2019-10-05Merge PR #10763: Fix syntax of reduction tactics when listing qualid to ↵Vincent Laporte
reduce or not. Reviewed-by: jfehrle
2019-10-04Improve language.Théo Zimmermann
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2019-10-04Merge PR #9772: [Stdlib] OrderedType: do not pollute the “core” hint ↵Pierre-Marie Pédrot
database Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2019-10-04Merge PR #10798: Loosen restrictions on mixing universe mono/polymorphism in ↵Pierre-Marie Pédrot
sections Reviewed-by: ppedrot
2019-10-04Allow SProp default onGaëtan Gilbert
2019-10-04[Stdlib] OrderedType: do not pollute the “core” hint databaseVincent Laporte
2019-10-03Improved handling of micromega cachesFrédéric Besson
- Specialised hash and equality functions. Avoid collisions in extreme scenarios. - Flags to disable the use of the caches. fixes #10772
2019-10-02Loosen restrictions on mixing universe mono/polymorphism in sectionsGaëtan Gilbert
We disallow adding univ constraints wich refer to polymorphic universes, and monomorphic constants and inductives when polymorphic universes or constraints are present. Every other combination is already correctly discharged by the kernel.
2019-09-25Adding documentation for the move of sections data to kernel.Pierre-Marie Pédrot
2019-09-19Fix #10420 Add dependent evar mapping info to outputJim Fehrle
2019-09-18Fix syntax of reduction tactics when listing qualid to reduce or not.Théo Zimmermann
2019-09-16Re-implementation of zifyFrédéric Besson
The logic is implemented in OCaml. By induction over the terms, guided by registered Coq terms in ZifyInst.v, it generates a rewriting lemma. The rewriting is only performed if there is some progress. If the rewriting fails (due to dependencies), a novel hypothesis is generated. This PR fixes #5155, fixes #8898, fixes #7886, fixes #10707, fixes #9848 ans fixes #10755. The zify plugin is placed in the micromega directory. (Though the reason is unclear, having it in a separate directory is bad for efficiency.) efficiency impact. There are also a few improvements of lia/lra that are piggybacked. - more aggressive pruning of useless hypotheses - slightly optimised conjunctive normal form - applies exfalso if conclusion is not in Prop - removal of Timeout in test-suite
2019-09-12Merge PR #10753: Release notes for 8.10+beta3.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-09-12Release notes for 8.10+beta3.Théo Zimmermann
2019-09-10Refman: To be compatible gtk2/gtk3, not mentioning GTK+ version explicitely.Hugo Herbelin
2019-09-10Fixing coqide doc about location of "coqiderc" and "coqide.bindings".Hugo Herbelin
2019-09-03Add missing index for From ... Require ...Théo Zimmermann
2019-08-26Document `Template Check` flag and add changelog entry for 9918Matthieu Sozeau
Fix changelog entry Fix build of the user manual Markup fixes from Théo Zimmermann Update doc and changelog and improve error messages.
2019-08-24[dune] Migrate static Dune files to Dune 1.10Emilio Jesus Gallego Arias
This improves error reporting. Addendum to #10515
2019-08-23[doc] Fix documentation of schedule-vioEmilio Jesus Gallego Arias
Master version of the fix for #10679
2019-08-20Merge PR #10291: Controlling typing flags with commands (no attribute)Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2019-08-16Fix quoting in 8.9 changelog entry.Théo Zimmermann
2019-08-16Universe Checking instead of Universes CheckingSimonBoulier
2019-08-16Add documentation for typing flags.SimonBoulier
2019-08-08Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations ↵Maxime Dénès
involving & Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: gares Ack-by: ggonthier Ack-by: herbelin Reviewed-by: maximedenes Ack-by: vbgl
2019-08-08[ssr] Refactor under's Setoid generalization to ease stdlib2 portingErik Martin-Dorel
Changes: * Add ssrclasses.v that redefines [Reflexive] and [iff_Reflexive]; * Add ssrsetoid.v that links [ssrclasses.Reflexive] and [RelationClasses.Reflexive]; * Add [Require Coq.ssr.ssrsetoid] in Setoid.v; * Update ssrfwd.ml accordingly, using a helper file ssrclasses.ml that ports some non-exported material from rewrite.ml; * Some upside in passing: ssrfwd.ml no more depends on Ltac_plugin; * Update doc and tests as well. Summary: * We can now use the under tactic in two flavors: - with the [eq] or [iff] relations: [Require Import ssreflect.] - or a [RewriteRelation]: [Require Import ssreflect. Require Setoid.] (while [ssreflect] does not require [RelationClasses] nor [Setoid], and conversely [Setoid] does not require [ssreflect]). * The file ssrsetoid.v could be skipped when porting under to stdlib2.
2019-08-06[ssr] under: extend ssreflect.v to generalize iff to any setoid eqErik Martin-Dorel
* Add an extra test with an Equivalence. * Update the doc accordingly.
2019-08-05Merge PR #10624: Remove reference to removed option Printing Primitive ↵Théo Zimmermann
Projection Compatibility Reviewed-by: Zimmi48
2019-08-05Remove reference to removed option Printing Primitive Projection CompatibilityJim Fehrle
2019-08-02Copy edit the Ltac2 documentationTej Chajed
2019-07-30Merge PR #10430: [Extraction] Add support for primitive integersMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-07-29Document changes by PR 10324Vincent Laporte
White spaces are forbidden in the “&ident” syntax for ltac2 references.
2019-07-29Merge PR #10548: Refine documentation of tokensThéo Zimmermann
Reviewed-by: Zimmi48 Ack-by: cpitclaudel Ack-by: herbelin
2019-07-29Merge PR #10574: Remove deprecated `Backtrack` commandEnrico Tassi
Reviewed-by: ejgallego Reviewed-by: gares
2019-07-28Update documentation on tokens, use "int" and "num"Jim Fehrle
for integers and natural nums
2019-07-26Remove the tactic wizard, as it has not worked for several years and no one ↵Guillaume Melquiond
complained (fixes #10580).
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-25 03:47:19 +0000