aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2020-11-05Changelog for 8.12.1.Théo Zimmermann
2020-11-05Merge PR #12218: Numeral notations for non inductive typescoqbot-app[bot]
Reviewed-by: herbelin Reviewed-by: JasonGross Reviewed-by: jfehrle Ack-by: Zimmi48
2020-11-05Merge PR #13301: Fixes #13298: Search applied to primitive projections needs ↵coqbot-app[bot]
a correct typing environment Reviewed-by: SkySkimmer
2020-11-05Add changelogPierre Roux
2020-11-05Rename Dec and HexDec to Decimal and HexadecimalPierre Roux
As noted by Hugo Herbelin, Dec is rather used for "decidable".
2020-11-05[refman] Add an example for number notationsPierre Roux
As suggested by Jim Fehrle while reviewing #12218
2020-11-05[string notation] Handle parameterized inductives and non inductivesPierre Roux
2020-11-05Merge numeral and string notation pluginsPierre Roux
2020-11-05[numeral notation] Add support for parameterized inductivesPierre Roux
2020-11-05[numeral notation] Handle implicit argumentsPierre Roux
2020-11-05[numeral notation] Specify RPierre Roux
2020-11-05[numeral notation] Document the via ... using ... optionPierre Roux
2020-11-04[numeral notation] Adding the via ... using ... optionPierre Roux
This enables numeral notations for non inductive types by pre/postprocessing them to a given proxy inductive type. For instance, this should enable the use of numeral notations for R.
2020-11-04Regenerate the grammar description file.Pierre-Marie Pédrot
2020-11-04Document the syntax addition.Pierre-Marie Pédrot
2020-11-04Adding change log for #13301.Hugo Herbelin
2020-11-03Merge PR #13293: Doc: added "Arguments" removing implicit argumentscoqbot-app[bot]
Reviewed-by: jfehrle Reviewed-by: Zimmi48
2020-11-03Merge PR #13092: Fixing #13078: stack overflow and anomalies with binding ↵coqbot-app[bot]
notations in patterns Reviewed-by: ejgallego Ack-by: ppedrot Ack-by: LasseBlaauwbroek
2020-11-03improved documentation of arguments commandFabian Kunze
2020-11-02Merge PR #13183: attribute #[using] for Definition and Fixpointcoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: herbelin Ack-by: Zimmi48
2020-11-02Merge PR #13247: Fixes #13241: nested Ltac functions wrongly reporting error ↵Pierre-Marie Pédrot
on the inner calls Reviewed-by: ppedrot
2020-11-02Doc: added "Arguments" removing implicit argumentsFabian Kunze
2020-11-02[doc] attribute #[using]Enrico Tassi
2020-11-02add changelogEnrico Tassi
2020-10-30Add change log for #13145.Hugo Herbelin
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-10-30Renaming numnotoption into number_modifierPierre Roux
2020-10-30Renaming Numeral.v into Number.vPierre Roux
2020-10-28Adding changelog for #13247.Hugo Herbelin
2020-10-27Change a few nonterminal names in mlgs and update doc to matchJim Fehrle
2020-10-27Rename tac2type -> ltac2_type,Jim Fehrle
typ_param -> ltac2_typevar, tac2expr -> ltac2_expr
2020-10-27Rename misc nonterminalsJim Fehrle
2020-10-27Rename tactic_expr -> ltac_exprJim Fehrle
2020-10-27Rename operconstr -> termJim Fehrle
2020-10-26Merge PR #12768: Granting wish #12762: warning on duplicated catch-all ↵coqbot-app[bot]
pattern-matching clause with unused named variable Reviewed-by: jfehrle Reviewed-by: vbgl Ack-by: gares
2020-10-25Merge PR #12936: Convert misc chapters to prodn, update syntaxcoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: mattam82 Ack-by: pi8027 Ack-by: herbelin Ack-by: gares Ack-by: fajb Ack-by: proux01
2020-10-24Convert misc chapters to prodnJim Fehrle
2020-10-23Correct doc using :>>Gaëtan Gilbert
The cast keywords are <: and <<:, not :>/:>> :>> stopped being a keyword in #13106
2020-10-22Make no match/multiple match for tacn/cmd an errorJim Fehrle
Always generate prodn* files if edits succeed
2020-10-22Merge PR #11924: Add style for smallcaps.coqbot-app[bot]
Reviewed-by: jfehrle
2020-10-20Merge PR #13214: Better message for doc_grammar; avoid an infinite SPLICE loopcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-10-20Add some missing smallcaps.Théo Zimmermann
2020-10-20[zify] Use flag for Z.to_euclidean_division_equations.Frédéric Besson
Update doc/sphinx/addendum/micromega.rst Co-authored-by: Jason Gross <jasongross9@gmail.com> Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-10-20[zify] Add support for Int63.intFrédéric Besson
Update doc/sphinx/addendum/micromega.rst Co-authored-by: Jason Gross <jasongross9@gmail.com> Update theories/micromega/ZifyInt63.v Co-authored-by: Jason Gross <jasongross9@gmail.com>
2020-10-19Better message and avoid an infinite SPLICE loopJim Fehrle
2020-10-19Add style for smallcaps.Théo Zimmermann
Co-authored-by: Clément Pit-Claudel <clement.pitclaudel@live.com>
2020-10-19Adding change log for #13092.Hugo Herbelin
2020-10-16Add change log for #13166.Hugo Herbelin
2020-10-15Merge PR #13140: Documenting Set Printing Goal Names + a small goal display fixcoqbot-app[bot]
Reviewed-by: ejgallego Reviewed-by: Zimmi48
2020-10-12Merge PR #13185: Add missing ";" in Record grammarcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-10-12Add missing ";" in record grammarJim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-14 22:25:42 +0000