| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-04-14 | [Sphinx] Move chapter 9 to new infrastructure. | Théo Zimmermann | |
| 2018-03-09 | Merge PR #6820: Tacticals assert_fails and assert_succeeds | Maxime Dénès | |
| 2018-03-06 | [compat] Remove "Shrink Abstract" | Emilio Jesus Gallego Arias | |
| Following up on #6791, we the option "Shrink Abstract". | |||
| 2018-02-28 | Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross). | Hugo Herbelin | |
| 2018-01-03 | add optimize_heap tactic for #6488 | Paul Steckler | |
| 2017-12-19 | Fix typo in the refman. | Théo Zimmermann | |
| 2017-12-14 | Add documentation for time_constr | Jason Gross | |
| 2017-12-14 | Add doc+changelog entries for new LtacProf tactics | Jason Gross | |
| 2017-12-11 | Remove deprecated appcontext and corresponding documentation. | Théo Zimmermann | |
| 2017-12-01 | clarify operation of sequences, #6095 | Paul Steckler | |
| 2017-11-06 | Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]", | Samuel Gruetter | |
| not "first [ progress tac1 | progress tac2 ]". And add a missing backslash. | |||
| 2017-09-29 | [vernac] Remove `Qed exporting` syntax. | Emilio Jesus Gallego Arias | |
| We don't gain anything from the kernel yet as transparent constants _do_ require the `side_eff` exporting machinery. Next step, understand why. | |||
| 2017-09-22 | Avoid generated names for html pages of the reference manual (bug #4742). | Guillaume Melquiond | |
| 2017-07-11 | Sync the manual with the deprecation warnings. | Théo Zimmermann | |
| 2017-07-04 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-06-26 | Merge PR#756: Fix Bug #5574, document function scope | Maxime Dénès | |
| 2017-06-23 | Fix Bug #5574, document function scope | Paul Steckler | |
| 2017-06-13 | Document evar naming syntax. | Théo Zimmermann | |
| 2017-05-27 | Documenting the existence of first and solve as Ltac definitions. | Pierre-Marie Pédrot | |
| 2017-05-11 | Add documentation for Set Ltac Batch Debug | Jason Gross | |
| 2017-04-25 | Mark transparent_abstract as risky in docs | Jason Gross | |
| As per Enrico's request. | |||
| 2017-04-25 | Add transparent_abstract tactic | Jason Gross | |
| 2016-09-30 | Merge remote-tracking branch 'github/pr/280' into v8.6 | Maxime Dénès | |
| Was PR#280: Document that [Reset Ltac Profile] is not synchronized with the document state | |||
| 2016-09-28 | Merge remote-tracking branch 'github/pr/232' into v8.6 | Maxime Dénès | |
| Was PR#232: Fix the parsing of goal selectors. | |||
| 2016-09-16 | Doc: [Reset Ltac Profile] is not synchronized | Jason Gross | |
| 2016-09-07 | Fix a typo in the reference manual | Jason Gross | |
| 2016-08-17 | In docs, fix command to reset Ltac profiling | Paul Steckler | |
| 2016-06-30 | Update the documentation for goal selectors. | Cyprien Mangin | |
| 2016-06-17 | par: like all: but in parallel | Enrico Tassi | |
| This commit documents par:, fixes its semantics so that is behaves like all:, supports (toplevel) abstract and optimizes toplevel solve. `par: solve [tac]` is equivalent to `Ltac tac1 := solve[tac]...par: tac1` but is optimized for failures: if one goal fails all are aborted immediately. `par: abstract tac` runs abstract on the generated proof terms. Nested abstract calls are not supported. | |||
| 2016-06-14 | Add documentation for goal selectors. | Cyprien Mangin | |
| 2016-06-05 | Make Ltac Profiling an setting | Jason Gross | |
| 2016-06-05 | Synchronize the profiler state with the document | Jason 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 @herbelin | Jason 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-05 | Add LtacProf documentation | Jason Gross | |
| 2016-06-05 | Adding the Print Ltac Signature command. | Pierre-Marie Pédrot | |
| 2015-12-18 | TYPOGRAPHY: correction of one particular error in the Reference Manual | Matej Kosik | |
| 2015-10-19 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-18 | Reference Manual: Applying standard style recommendation about not | Hugo Herbelin | |
| starting a sentence with a symbolic expression. | |||
| 2015-10-12 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-11 | Documenting matching under binders. | Hugo Herbelin | |
| 2015-08-22 | Documenting the Shrink Abstract option. | Pierre-Marie Pédrot | |
| 2015-03-22 | Qed export -> Qed exporting | Enrico Tassi | |
| 2015-02-23 | Fixed doc of fresh (was already outdated before fixing #3233). | Pierre Courtieu | |
| 2015-02-17 | Separate index for vernacular options. | Maxime Dénès | |
| 2015-02-14 | Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior | Enrico Tassi | |
| Of course such proofs cannot be processed asynchronously | |||
| 2015-01-29 | Fix index of reference manual. | Guillaume Melquiond | |
| 2015-01-21 | Reference manual: fix typo in doc of [tryif/then/else]. | Arnaud Spiwack | |
| Fixes #3939. | |||
| 2015-01-14 | Reference manual: I had previously omitted the syntax entry for [> t1|…|tn]. | Arnaud Spiwack | |
| 2015-01-14 | Reference manual: document tryif/then/else. | Arnaud Spiwack | |
| 2015-01-14 | Reference manual: document multimatch. | Arnaud Spiwack | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |