aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
2020-01-09Merge PR #11164: [CS] allow Let variable to be canonicalPierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Reviewed-by: ppedrot
2020-01-08Add Set NativeCompute TimingJason Gross
The command `Set NativeCompute Timing` causes calls to `native_compute` (as well as kernel calls to the native compiler) to emit separate timing information about compilation, execution, and reification. This allows more fine-grained timing of the native compiler without needing to set the `-debug` flag.
2020-01-08Add note about default goal selector next to bullet docsGaëtan Gilbert
Close #11036
2020-01-08Add documentation for extraction of ascii and string literalsMaxime Dénès
2020-01-08[refman] [changelog] Announce omega replacement.Théo Zimmermann
2020-01-08Trailing implicit: Maxime's suggestionsSimonBoulier
2020-01-07Merge PR #11369: [refman] Correct manual about implicit parameters in inductivesThéo Zimmermann
Reviewed-by: Zimmi48
2020-01-07Correct manual about implicit parameters in inductives.SimonBoulier
2020-01-07Trailing implicit error: documentationSimonBoulier
2020-01-06doc: mention limitation of bidi hints vs programGaëtan Gilbert
No example as I'm not familiar enough with Program to make one.
2020-01-06Merge PR #11340: [refman] Fix bad quoting practice leftover from Sphinx ↵Clément Pit-Claudel
migration. Reviewed-by: jfehrle
2020-01-03Merge PR #11343: fix: Shorten ssrsetoid.v to fix TC performance issueEnrico Tassi
Reviewed-by: gares
2019-12-31Merge PR #11325: [refman] Add missing s.Pierre-Marie Pédrot
Reviewed-by: jfehrle
2019-12-29Remove :flag: that appears in the outputJim Fehrle
2019-12-29[refman] Fix bad quoting practice leftover from Sphinx migration.Théo Zimmermann
2019-12-29Merge PR #11314: Convert productionlists in the Gallina chapter up to the ↵Théo Zimmermann
Vernacular section to prodns Reviewed-by: Zimmi48
2019-12-29Merge PR #11183: Enhance prodn in .rst doc files to support multiple ↵Théo Zimmermann
productions in a prodn Ack-by: Zimmi48 Ack-by: cpitclaudel
2019-12-28Convert productionlists to prodnsJim Fehrle
2019-12-28Update doc/sphinx/language/gallina-extensions.rstKazuhiko Sakaguchi
Co-Authored-By: Cyril Cohen <CohenCyril@users.noreply.github.com>
2019-12-28Extend `Print Canonical Projections` with a search functionalityKazuhiko Sakaguchi
The `Print Canonical Projections` command now can take constants and prints only the unification rules that involves or are synthesized from given constants.
2019-12-27docs: Update changes.rst w.r.t. ssrsetoid.v's simplificationErik Martin-Dorel
2019-12-25Show doc notations in boldfaceJim Fehrle
2019-12-24[Attributes] accept #[canonical] (Let|Definition)Enrico Tassi
2019-12-23Merge PR #11324: [refman] Mention Ltac2 in intro.Pierre-Marie Pédrot
Reviewed-by: jfehrle
2019-12-23Merge PR #10760: Make rapply handle all numbers of underscoresPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2019-12-22Apply suggestions from code reviewThéo Zimmermann
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2019-12-22[refman] Mention Ltac2 in intro.Théo Zimmermann
2019-12-22[refman] Add missing s.Théo Zimmermann
2019-12-20Coherence checking for coercionsKazuhiko Sakaguchi
This change improves the relaxed ambiguous path condition of coercions (#9743) to check that any circular inheritance path of `C >-> C` is definitionally equal to the identity function of the class `C`. Moreover, for a new inheritance path `p : C >-> D` and existing (valid) one `q : C >-> D`, the new mechanism does not report the ambiguity of `p` and `q` if they have a common element, that is to say: `p = p1 @ [c] @ p2` and `q = q1 @ [c] @ q2` for some coercion `c` and inheritance paths `p1`, `p2`, `q1`, and `q2`. In that case, convertibility of `p1` and `q1`, also, `p2` and `q2` should be checked; thus, checking the ambiguity of `p` and `q` is redundant with them. If the new mechanism does not report any ambiguous path, the inheritance graph must be coherent [Barthe 1995, Sect. 3.2] [Saïbi 1997, Sect. 7]: 1. for any circular path `p : C >-> C`, `p` is definitionally equal to the identity function, and 2. for any two paths `p, q : C >-> D`, `p` and `q` are convertible. [Barthe 1995] Gilles Barthe, Implicit coercions in type systems, In: TYPES '95, LNCS, vol 1158, Springer, 1996, pp 1-15. [Saïbi 1997] Amokrane Saïbi, Typing algorithm in type theory with inheritance, In: POPL '97, ACM, 1997, pp 292-301.
2019-12-14Make prodn look more like productionlistJim Fehrle
2019-12-14Fix refine and eapply to mark shelved goals as non-resolvable, alwaysMatthieu Sozeau
Check that we don't regress on PR #10762 example Fix regression discovered by Arthur in PR #10762 Fix script of #10298 which was relying on breaking semantics for `eapply` Add doc Add comment in clenvtac Actually, always mark shelved goals as unresolvable Update doc to reflect semantics w.r.t. shelved subgoals
2019-12-12Fix #11195 and add other improvements: try loading .vio (and not just .vo) ↵charguer
if the .vos file is empty, rename -quick to -vio, dump empty .vos when producing .vio, dump empty .vos and .vok files when producing .vo from .vio.
2019-12-04[dune] Update to dune language version 2.0Emilio Jesus Gallego Arias
This is the minimal set of changes requires for Coq to build under 2.0 mode. We may likely take advantage of some more new features. Note that Dune 2.0 requires OCaml >= 4.06.0, OPAM allows to use Dune in older versions as it will install a secondary compiler.
2019-12-03Merge PR #11162: [CS] support #[local] attributeMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2019-12-02[CS] support #[local] attributeEnrico Tassi
2019-12-02List of 8.11 contributors and stats.Théo Zimmermann
2019-12-02Merge redundant consecutive changelog entries on reals.Théo Zimmermann
2019-12-02Highlight refine attribute for Instance.Théo Zimmermann
2019-12-02Warn more clearly about incompatibilities coming from #10476.Théo Zimmermann
2019-12-028.11 release notes.Matthieu Sozeau
2019-12-02Move unreleased changelog to new 8.11 section.Théo Zimmermann
2019-12-02Merge PR #10575: Clean up deprecationsThéo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: silene
2019-12-01Merge PR #11185: Remove deprecated Typeclasses Axioms Are Instances.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: cpitclaudel
2019-11-30Actually deprecate the `cutrewrite` tacticMaxime Dénès
The manual was already saying that it was deprecated, but no warning was emitted. Fixes #10572
2019-11-30Deprecation annotation for `convert_concl_no_check`Maxime Dénès
2019-11-29Remove deprecated Typeclasses Axioms Are Instances.Théo Zimmermann
2019-11-28Release notes for Coq 8.10.2Vincent Laporte
2019-11-27weaker then -> weaker thanlarsr
2019-11-26Remove `rapply` tactic notation in favor of just the tacticJason Gross
This increases backwards compatibility. If desired, we can add a tactic notation to simplify the spec of `rapply` in the future if we want.
2019-11-26Make rapply handle all numbers of underscoresJason Gross
Also add a tactic notation so that it takes in uconstrs by default. Also add some basic tests for `rapply`. Also document rapply in the manual
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 00:01:08 +0000