| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-08-01 | Detyping functions are now operating on EConstr.t. | Pierre-Marie Pédrot | |
| This was already the case, but the API was not exposing this. | |||
| 2017-08-01 | Binding more primitive tactics. | Pierre-Marie Pédrot | |
| 2017-08-01 | Fix typos. Improve wording. | Sam Pablo Kuper | |
| 2017-08-01 | More in documentation. | Pierre-Marie Pédrot | |
| 2017-08-01 | Improve style slightly | Sam Pablo Kuper | |
| per @aspiwack's comments in [this pull request review](https://github.com/coq/coq/pull/940). | |||
| 2017-08-01 | Move glob_constr_ltac_closure to evar_refiner. | Maxime Dénès | |
| 2017-08-01 | Merge PR #933: Fix documentation of Hint Mode (bug #4911). | Maxime Dénès | |
| 2017-08-01 | Merge PR #932: Fix shuffled documentation. | Maxime Dénès | |
| 2017-08-01 | Merge PR #929: Add missing paragraph to introduction | Maxime Dénès | |
| 2017-08-01 | Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas). | Maxime Dénès | |
| 2017-08-01 | Merge PR #926: test-suite uses Extraction TestCompile | Maxime Dénès | |
| 2017-08-01 | Merge PR #925: Document Extraction TestCompile | Maxime Dénès | |
| 2017-08-01 | Merge PR #921: [make] remove compat5 file. | Maxime Dénès | |
| 2017-08-01 | Merge PR #919: Remove a few useless evar-normalizations in printing code. | Maxime Dénès | |
| 2017-08-01 | Merge PR #917: Moving --print-version to -print-version for consistency. | Maxime Dénès | |
| 2017-08-01 | Merge PR #913: Less allocations in Detyping | Maxime Dénès | |
| 2017-08-01 | Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709) | Maxime Dénès | |
| 2017-08-01 | Merge PR #893: Removing default evar-normalization for ARGUMENT EXTEND. | Maxime Dénès | |
| 2017-08-01 | Merge PR #834: Adding support for recursive notations of the form "x , .. , ↵ | Maxime Dénès | |
| y , z". | |||
| 2017-08-01 | Merge PR #806: closing bug 5315 | Maxime Dénès | |
| 2017-08-01 | Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options. | Maxime Dénès | |
| 2017-08-01 | adding a comment to explain the change | Julien Forest | |
| 2017-08-01 | Fixup doc | Pierre-Marie Pédrot | |
| 2017-08-01 | Fixup doc | Pierre-Marie Pédrot | |
| 2017-08-01 | Adding documentation from the CEP. | Pierre-Marie Pédrot | |
| 2017-08-01 | Do not thunk notations preemptively. | Pierre-Marie Pédrot | |
| One has to rely on the 'thunk' token to produce such thunks. | |||
| 2017-08-01 | Adding new scopes for standard Ltac structures. | Pierre-Marie Pédrot | |
| 2017-08-01 | solving b1859 | Julien Forest | |
| 2017-07-31 | Fix incorrect use of "At the end". | Sam Pablo Kuper | |
| 2017-07-31 | Minor grammar fix: replace a "then" with a "so". | Sam Pablo Kuper | |
| 2017-07-31 | Replace jarring use of "Remark" with "Note" | Sam Pablo Kuper | |
| or with nothing at all, to improve readability for native English speakers. Editors may wish to remove such constructions altogether in future revisions, per general style guidance such as: - https://en.wikipedia.org/wiki/Wikipedia:%22Note_that%22_is_unnecessary - https://english.stackexchange.com/a/238142/7318 - http://blog.apastyle.org/apastyle/2015/09/principles-of-writing-how-to-avoid-wordiness.html | |||
| 2017-07-31 | Update documentation of cumulativity | Amin Timany | |
| 2017-07-31 | Improve errors for cumulativity when monomorphic | Amin Timany | |
| We now only issue an error for locally specified (non)cumulativity whenever it is the context (set locally or globally) is monorphic. | |||
| 2017-07-31 | Change the option for cumulativity | Amin Timany | |
| 2017-07-31 | Fix typo and Add Jason's example to the doc | Amin Timany | |
| 2017-07-31 | Improve documentation of cumulativity | Amin Timany | |
| 2017-07-31 | Add Jason's example of fun-ext with cumulativity | Amin Timany | |
| 2017-07-31 | Add test for NonCumulative inductives | Amin Timany | |
| 2017-07-31 | Issue error on monomorphic cumulative inductives | Amin Timany | |
| 2017-07-31 | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead | Maxime Dénès | |
| 2017-07-31 | Merge PR #746: Timing on ci via coq_makefile for various projects | Maxime Dénès | |
| 2017-07-31 | [general] Remove spurious dependency of highparsing on toplevel. | Emilio Jesus Gallego Arias | |
| `G_vernac` was depending on `toplevel` just for parsing the compat number information. IMHO this was not the right place, so I have moved the parsing bits to parsing and updated the files. This allows to finally separate the `toplevel` from Coq, which avoids linking it in alternative toplevels. | |||
| 2017-07-31 | better `try with` scope in `discr_positions` | amblaf | |
| 2017-07-31 | Correcting [build_discriminator] to make the test-suite pass | amblaf | |
| 2017-07-31 | Replacing tclENV with the goal environment | amblaf | |
| In functions match_eqdec and check_unused_names | |||
| 2017-07-31 | env, sigma as first arguments of functions | amblaf | |
| 2017-07-31 | Remove references to Global.env in tactics/*.ml | amblaf | |
| Only in ml files that are not related to Coq commands | |||
| 2017-07-30 | Exporting more internals from Coq implementation. | Pierre-Marie Pédrot | |
| 2017-07-29 | Drop paragraph mentioning Addendum as separate doc. | Théo Zimmermann | |
| As suggested by @herbelin. | |||
| 2017-07-29 | closing bug 5315 | Julien Forest | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |