aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
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-29Merge PR #10931: Add types of changes to changelog entries.Emilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego
2019-11-28Release notes for Coq 8.10.2Vincent Laporte
2019-11-28Update README and make-changelog tool following introduction of changelog types.Théo Zimmermann
2019-11-28[changelog] Add types to changelog entries.Théo Zimmermann
Types of changes are defined in the list defined by Keep a Changelog 1.0.0 (https://keepachangelog.com/en/1.0.0/): - Added - Changed - Deprecated - Fixed - Removed We exclude the type Security for now, even for soundness fixes, because the process of handling security vulnerabilities is different from anything we follow right now.
2019-11-28Fix extension of changelog file.Théo Zimmermann
2019-11-27Merge PR #11187: Remove deprecated commands `AddPath`, `AddRecPath` and ↵Emilio Jesus Gallego Arias
`DelPath` Reviewed-by: ejgallego
2019-11-27Changelog entry for #11187.Théo Zimmermann
2019-11-27Correcting unintended changelog message for #11090 (coercion+notation ↵Hugo Herbelin
regression).
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
2019-11-27weaker then -> weaker thanlarsr
2019-11-26Merge PR #11090: Printing of coercions to which a notation is associated: a ↵Emilio Jesus Gallego Arias
refined version of #8890 which prevents #11033. Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares
2019-11-25Add more development setup instructions for tutorialsTalia Ringer
2019-11-25Minor fix in doc for [unfold]Gaëtan Gilbert
Close #9634
2019-11-22Merge PR #11136: Adding `inj_compr` lemma in ssrfun.Enrico Tassi
Ack-by: Zimmi48 Reviewed-by: gares
2019-11-21A refined version of #8890 which prevents #11033.Hugo Herbelin
We restrict #8890 so that it looks for a notation only for the fully applied coercion.
2019-11-21Merge PR #11145: Document -vos flag for coqdepEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-11-21Merge PR #11132: Fixing bugs in the computation of implicit arguments for ↵Emilio Jesus Gallego Arias
`Fixpoint` with a let binder Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-11-21Merge PR #10614: Update the Gallina grammar in doc, "Terms" sectionThéo Zimmermann
Ack-by: Zimmi48
2019-11-21Document -vos flag for coqdepGaëtan Gilbert
2019-11-21Update ↵Hugo Herbelin
doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-11-21Merge PR #11075: load .vo when .vos is missing + misc vos changesEmilio Jesus Gallego Arias
Reviewed-by: gares Reviewed-by: silene
2019-11-21Taking @Zimmi48's comment into accountCyril Cohen
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
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-20Merge PR #11119: 8.10-backportable part of #10575Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-11-20From CoqIDE or -vos or -vok compilation, load .vo when .vos is missing ↵charguer
(fixing bug #11057). With this new behavior, it is not needed to .vos files in user contribs. Also, this commit adds a feature: upon creation of a .vo file, an empty .vok file is touched.
2019-11-19Fixing bugs in the computation of implicit arguments for fix with a let binder.Hugo Herbelin
2019-11-19coq_makefile: support COQBIN with no ending /Gaëtan Gilbert
Close #6460
2019-11-19added changelog entryCyril Cohen
2019-11-16Merge PR #10996: Refine Instance returnsPierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-11-15Update doc/changelog/04-tactics/10998-zify-complements.rstKazuhiko Sakaguchi
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-11-15Add missing zify class instancesKazuhiko Sakaguchi
Add missing zify class instances for `Pos.pred_double`, `Pos.pred_N`, `Pos.of_nat`, `Pos.add_carry`, `Pos.pow`, `Pos.square`, `Z.pow`, `Z.double`, `Z.pred_double`, `Z.succ_double`, `Z.square`, `Z.div2`, `Z.quot2`, `isZero`, and `isLeZero`. Instances for `isZero` and `isLeZero` are useful to provide new zify instances by using Micromega tactics.
2019-11-14Merge PR #10979: Fix doc for universes(foo) attributesThéo Zimmermann
Reviewed-by: Zimmi48
2019-11-14Fix doc for universes(foo) attributesGaëtan Gilbert
Fix #10570
2019-11-14Merge PR #11100: small documentation fixesThéo Zimmermann
Reviewed-by: Zimmi48 Ack-by: cpitclaudel
2019-11-14doc fixesAntonio Nikishaev
2019-11-14Restore documentation of `Typeclasses Axioms Are Instances`Maxime Dénès
This documentation seems to have been lost after it was introduced by 0ad26633a4589d77de1f864733d1d953dab9ea91 We also document that this flag is deprecated.
2019-11-14Document recommended syntax for `firstorder`Maxime Dénès
Only the deprecated one was documentated, and the deprecation was not mentioned.
2019-11-13Return of Refine Instance as an attribute.Gaëtan Gilbert
We can now do `#[refine] Instance : Bla := bli.` to enter proof mode with `bli` as a starting refinement. If `bli` is enough to define the instance we still enter proof mode, keeping things nicely predictable for the stm.
2019-11-11Run update-compat script with --release option.Théo Zimmermann
This should ideally have been done before the 8.11 branching.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 15:47:31 +0000