aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2020-07-05Merge PR #12613: Remove deprecated (in 8.8 #6277) coqchk -IPierre-Marie Pédrot
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-07-03Merge PR #10390: UIP in SPropMaxime Dénès
2020-07-02Merge PR #12572: Correctly classify variables as being unfoldable in dnet pat...Gaëtan Gilbert
2020-07-01UIP in SPropGaëtan Gilbert
2020-07-01Remove deprecated (in 8.8 #6277) coqchk -IGaëtan Gilbert
2020-07-01Merge PR #12596: Credit Erik Martin-Dorel for work on Docker.Emilio Jesus Gallego Arias
2020-06-29Merge PR #12541: Fix #12228 negative integers not accepted in ltac integer_listPierre-Marie Pédrot
2020-06-29Merge PR #12372: [declare] Refactor constant information into a record.Gaëtan Gilbert
2020-06-27Merge PR #12583: [test-suite] Fix dependencies of modules/ filesGaëtan Gilbert
2020-06-26Mention VSCoq with respect to _CoqProjectCarl Patenaude-Poulin
2020-06-26[declare] Improve organization of proof/constant information.Emilio Jesus Gallego Arias
2020-06-26[declare] Reify Proof.t API into the Proof module.Emilio Jesus Gallego Arias
2020-06-26[declare] [api] Removal of duplicated type aliases.Emilio Jesus Gallego Arias
2020-06-26[declare] Refactor constant information into a record.Emilio Jesus Gallego Arias
2020-06-26[declare] Move proof information to declare.Emilio Jesus Gallego Arias
2020-06-26Credit Erik Martin-Dorel for work on Docker.Théo Zimmermann
2020-06-24[test-suite] Fix dependencies of modules/ filesJason Gross
2020-06-23Correctly classify variables as being unfoldable in dnet patterns.Pierre-Marie Pédrot
2020-06-23Merge PR #12562: CoqIDE: accept to open files with invalid namesMichael Soegtrop
2020-06-23Merge PR #12552: Add a pre-hook mechanism for the `zify` tacticFrédéric Besson
2020-06-22CoqIDE: accept to open files with invalid namesVincent Laporte
2020-06-21Add index for coqdoc.Théo Zimmermann
2020-06-20Add a pre-hook mechanism for the `zify` tacticKazuhiko Sakaguchi
2020-06-18Fix #12228 negative integers not accepted in ltac integer_listPierre Roux
2020-06-17tactics.rst: readd `cbv`Paolo G. Giarrusso
2020-06-14Update zify documentationFrédéric Besson
2020-06-14[micromega] native support for boolean operatorsFrédéric Besson
2020-06-11Merge PR #12481: Minor improvements to the sections on basics and sorts.Emilio Jesus Gallego Arias
2020-06-11Merge PR #12423: Remove info tactic, deprecated in 8.5Pierre-Marie Pédrot
2020-06-10Update changelog for 8.12+beta1.Théo Zimmermann
2020-06-09Merge PR #12484: Fix #12483 Incorrect specification of PrimFloat.lebGuillaume Melquiond
2020-06-09Merge PR #12186: CReal: changed epsilon for modulus of convergence from 1/n t...Vincent Semeria
2020-06-09Merge sections on functions and function types.Théo Zimmermann
2020-06-09Minor improvements to the section on sorts.Théo Zimmermann
2020-06-09Minor improvements to the section on basics.Théo Zimmermann
2020-06-09Merge PR #12103: Convert Ltac chapter to prodnThéo Zimmermann
2020-06-09Summary of changes for 8.12Matthieu Sozeau
2020-06-09CReal: changed epsilon for modulus of convergence from 1/n to 2^zMichael Soegtrop
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-06-08Make automatic name generation for directives more consistent:Jim Fehrle
2020-06-08Add NOTINRSTS nonterminal to suppress messagesJim Fehrle
2020-06-08Report an error for empty (sub)productionsJim Fehrle
2020-06-08Add MOVEALLBUT operationJim Fehrle
2020-06-08Refactor SELF code for clarityJim Fehrle
2020-06-08Fix 12483Pierre Roux
2020-06-07[sphinx] Fix regexp used in coqdomain.CoqtopBlocksTransform.split_linesClément Pit-Claudel
2020-06-07Merge PR #12473: Match only a single line as the coqtop prompt in coqtop:: di...Clément Pit-Claudel
2020-06-06Match only a single line as the coqtop promptJim Fehrle
2020-06-06Merge PR #12380: Fix #12361 (indexing issues in the PDF)Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 09:48:38 +0000