aboutsummaryrefslogtreecommitdiff
path: root/doc/refman
AgeCommit message (Collapse)Author
2017-04-25Mark transparent_abstract as risky in docsJason Gross
As per Enrico's request.
2017-04-25Add transparent_abstract tacticJason Gross
2017-04-24refman: remember the old name of template polymorphism.Gaetan Gilbert
2017-04-12Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵Maxime Dénès
record fields.
2017-04-11Update RefMan-pre to mention template polymorphism.Gaetan Gilbert
2017-04-11Use "template polymorphism" in the documentation.Gaetan Gilbert
2017-04-11Mention template polymorphism in the documentation.Gaetan Gilbert
Since About mentions it the doc should as well.
2017-04-09Merge PR#460: Turning the printing primitive projection compatibility flag ↵Maxime Dénès
off by default
2017-04-09Fixing #5420 as well as many related bugs due to miscounting let-ins.Hugo Herbelin
- Supporting let-ins in tactic "fix", and hence in interactive Fixpoint and mutual theorems. - Documenting more precisely the meaning of n in tactic "fix id n". - Fixing computation of recursive index at interpretation time in the presence of let-ins.
2017-04-07Merge PR#485: Document Show MatchMaxime Dénès
2017-04-07Turning the printing primitive projection parameter flag off by default.Hugo Herbelin
2017-04-07Turning the printing primitive projection compatibility flag off by default.Hugo Herbelin
2017-04-06Merge PR#455: Farewell decl_modeMaxime Dénès
2017-03-23Documenting the grammar {| ... |} syntax for building records.Hugo Herbelin
And an extra minor changes (use of zeroone when relevant, use of type rather than term).
2017-03-23Merge PR#433: doc: fix a French-ismMaxime Dénès
2017-03-22Fix some typos.Guillaume Melquiond
2017-03-22Merge PR#482: [toplevel] Remove unusable option -notopMaxime Dénès
2017-03-17Document Show Match, add ref to that in match variants/extensionsPaul Steckler
2017-03-14doc: fix a French-ismValentin Robert
2017-03-14[toplevel] Remove unusable option -notopEmilio Jesus Gallego Arias
Maxime points out that -notop cannot be used as the kernel requires all constants to belong into a module. Indeed: ``` $ rlwrap ./bin/coqtop -notop Coq < Definition foo := True. Toplevel input, characters 0-23: > Definition foo := True. > ^^^^^^^^^^^^^^^^^^^^^^^ Error: No session module started (use -top dir) Coq < Module M. Definition foo := True. End M. Module M is defined Coq < Locate foo. Constant If you see this, it's a bug.M.foo (shorter name to refer to it in current context is M.foo) ``` My rationale for the removal is that this kind of incomplete features are often confusing to newcomers ─ it has happened to me many times ─ as it can be seen for example in #397 .
2017-03-14Merge PR#438: Fix V7 syntax in refman.Maxime Dénès
2017-03-09Typo doc notations.Hugo Herbelin
2017-03-09Clarifying doc about interpretation of scopes in notations (#5386).Hugo Herbelin
2017-03-07Farewell decl_modeEnrico Tassi
This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests.
2017-02-20Fix V7 syntax in refman.Théo Zimmermann
2017-01-19Merge branch 'v8.6'Pierre-Marie Pédrot
2016-12-16Fix incorrect documentation that prevents successful compilation (bug #5265).Guillaume Melquiond
2016-12-07Merge branch 'v8.6'Pierre-Marie Pédrot
2016-12-06Fix broken documentation in presence of \zeroone{... \tt ...}.Guillaume Melquiond
The way \zeroone was defined, the \tt modifier was leaked outside the brackets, thus messing with the following text. There are a bunch of occurrences of this issue in the manual, so rather than turning all the \tt into \texttt, the definition of \zeroone is made more robust. Unfortunately, there is one single occurrence of \zeroone that does not support the more robust version. (Note that this specific usage of \zeroone is morally a bug, since it goes against all the LaTeX conventions.) So the commit also keeps the old leaky version of \zeroone around as \zeroonelax so that it can be used there.
2016-12-06Update documentation (bugs #5246 and #5251).Guillaume Melquiond
2016-12-05Change module for Coq loopPaul Steckler
2016-12-05the -byte option is deprecatedPaul Steckler
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-17Add missing label. Fixes broken ref.Théo Zimmermann
2016-11-16Revert more of a477dc for good measureMatthieu Sozeau
We stop failing automatically on non-declared-class nested or toplevel subgoals as in 8.5, instead of the previous a477dc behavior of shelving those goals and failing if shelved goals remained at the end of resolution. It means typeclass resolution during refinement is closer to all:typeclasses eauto. Hints in typeclass_instances for non-declared classes can be used during resolution of _nested_ subgoals when it is fired from type-inference, toplevel goals considered in this case are still only classes (as in 8.5 and before). The code that triggers the restriction to only declared class subgoals is commented. Revert changes to test-suite, adding test for #5203, #5198 is fixed too. Add corresponding tests in the test-suite (that will break if we, e.g. disallow non-class subgoals) and update the refman accordingly.
2016-11-15Revert part of a477dc, disallow_shelvedMatthieu Sozeau
In only_classes mode we do not try to implement a stricter semantics for shelved goals in 8.6. Leaving this for 8.7. Update the documentation as well. Remove a spurious printf call as well. Fix test-suite now that shelved goals are allowed
2016-11-14Do not mention "none" in warnings doc, as it is there for compatibility.Maxime Dénès
2016-11-10Update CHANGES and credits for 8.6beta1.Maxime Dénès
2016-11-08Merge remote-tracking branch 'github/pr/348' into v8.6Maxime Dénès
Was PR#348: Credits for 8.6
2016-11-08Update documentation of Arguments after recent changes.Maxime Dénès
2016-11-08Rewording from EnricoMatthieu Sozeau
2016-11-07After Emilio's comment.Matthieu Sozeau
2016-11-07Merge remote-tracking branch 'github/pr/339' into v8.6Maxime Dénès
Was PR#339: Documenting type class options, typeclasses eauto
2016-11-07Document two new variants of refineMatthieu Sozeau
They allow to call refine without doing typeclass resolution, allowing to use refine in typeclass hints.
2016-11-07More accurate contributor list.Matthieu Sozeau
Command used: git log v8.5..HEAD --pretty=format:"%an," | sort -k 2 | uniq with some manual postprocessing for login names, particles and multiple first names.
2016-11-07Hugo and Maxime's 2nd pass of commentsMatthieu Sozeau
2016-11-06Hugo's commentsMatthieu Sozeau
2016-11-06Maxime's commentsMatthieu Sozeau
2016-11-06Fixes from Enrico's reviewMatthieu Sozeau
2016-11-05Credits for 8.6Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 19:06:53 +0000