aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2016-06-16Revise syntax of Hint CutMatthieu Sozeau
As noticed by C. Cohen it was confusingly different from standard notation.
2016-06-16Merge 'pr/191' into trunkEnrico Tassi
2016-06-15typographyMatej Kosik
2016-06-14Add documentation for goal selectors.Cyprien Mangin
2016-06-14-async-proofs-delegation-threshold default value set to 0.03Enrico Tassi
Documentation also updated.
2016-06-14Merge remote-tracking branch 'origin/pr/173' into trunkEnrico Tassi
This is the "error resiliency" mode for STM
2016-06-14Merge branch "LtacProf for trunk" (PR #165).Pierre-Marie Pédrot
2016-06-13Univs: more robust Universe/Constraint decls #4816Matthieu Sozeau
This fixes the declarations of constraints, universes and assumptions: - global constraints can refer to global universes only, - polymorphic universes, constraints and assumptions can only be declared inside sections, when all the section's variables/universes are polymorphic as well. - monomorphic assumptions may only be declared in section contexts which are not parameterized by polymorphic universes/assumptions. Add fix for part 1 of bug #4816
2016-06-07typoMatej Kosik
2016-06-07typographyMatej Kosik
2016-06-07DocumentationEnrico Tassi
2016-06-05Make Ltac Profiling an settingJason Gross
2016-06-05Synchronize the profiler state with the documentJason Gross
This is suboptimal, because mutation leaves room for subtle bugs, but rewriting @tebbi's code to be functional was a pain, and not something I could figure out how to do easily. I'm working under the assumption that there is no sharing in a single treenode, which I'm not completely sure is valid. That said, a few simple tests seem to indicate that this works as expected.
2016-06-05-profileltac -> -profile-ltac, as per @herbelinJason Gross
https://github.com/coq/coq/pull/150#issuecomment-219141596 ```bash git grep --name-only profileltac | xargs sed s'/profileltac/profile-ltac/g' -i ```
2016-06-05Add LtacProf documentationJason Gross
2016-06-05Adding the Print Ltac Signature command.Pierre-Marie Pédrot
2016-06-03Fix build of documentation (broken for four months).Guillaume Melquiond
2016-05-15Fix a really small doc typoRicky Elrod
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-03In Regular Subst Tactic mode, ensure that the order of hypotheses isHugo Herbelin
preserved, which is a source of incompatibilities w.r.t. released 8.5 but which looks to me to be the only possible canonical behavior. This is I believe a better behavior than the Regular Subst Tactic behavior in the released 8.5 and 8.5pl1. There, the order of hypotheses in which substitutions happened was respected, but their interleaving with other hypotheses was not respected. So, I consider this to be a fix to the "Regular Subst Tactic" mode. Also added a more detailed "specification" of the "Regular" behavior of "subst" in the reference manual.
2016-05-02Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-28Update tutorial (fix bug #4699).Guillaume Melquiond
2016-04-24Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-12FIX: HTML version of Chapter 4 of the Reference ManualMatej Kosik
2016-04-12TYPOGRAPHY: adding missing \noindent macrosMatej Kosik
2016-04-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq ↵Matthieu Sozeau
into JasonGross-trunk-function_scope
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-24Document Hint Mode, cleanup Hint doc.Matthieu Sozeau
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-20Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.Maxime Dénès
2016-01-20Documenting Set Bullet Behavior.Hugo Herbelin
This is useful for restoring bullets after e.g. loading ssreflect. Hoping Arnaud is ok in documenting it.
2016-01-20Clarifying the documentation of tactics "cbv" and "lazy".Hugo Herbelin
Following a discussion on coq-club on Jan 13, 2016.
2016-01-15Thanks Hugo, but let's remain factual.Maxime Dénès
2016-01-14Updating and improving the documentation of intros patterns.Hugo Herbelin
In particular, documenting bracketing of last pattern on by default.
2016-01-13MMaps: remove it from final 8.5 release, since this new library isn't mature ↵Pierre Letouzey
enough In particular, its interface might still change (in interaction with interested colleagues). So let's not give it too much visibility yet. Instead, I'll turn it as an opam packages for now.
2016-01-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-12Referring to coq.inria.fr/stdlib for more on libraries and ltac-level tactics.Hugo Herbelin
2016-01-12Documenting dtauto and dintuition.Hugo Herbelin
2016-01-12Documenting options "Intuition Negation Unfolding", "Intuition Iff Unfolding".Hugo Herbelin
2016-01-12Documenting option 'Set Bracketing Last Introduction Pattern'.Hugo Herbelin
2016-01-12restore documentation of admitEnrico Tassi
2016-01-06Fix description of command-line options in the manual.Guillaume Melquiond
2015-12-18TYPOGRAPHY: correction of one particular error in the Reference ManualMatej Kosik
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-16Updating credits.Hugo Herbelin
2015-12-16Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".Guillaume Melquiond
2015-12-15Proof using: do not clear unused section hyps automaticallyEnrico Tassi
The option is still there, but not documented since it is too dangerous. Hints and type classes instances are not taking cleared variables into account.
2015-12-15Simplifying documentation of "assert form as pat".Hugo Herbelin
2015-12-15Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 08:19:00 +0000