aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
| | | | | | | * | | | | | | | | | | | Update Setoid.texGravatar larsr2017-08-02
| |_|_|_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The term of type `list nat` should be `(@nil nat)` instead of `(nil nat)`.
* | | | | | | | | | | | | | | | | | Makefile: 'make clean' now immune to the check for binary files without sourcesGravatar Pierre Letouzey2017-08-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a followup of 7d1fc15. Without this fix, you're warned of leftover files, but even a 'make clean' is then refused, so you cannot get rid of them easily (apart via a git clean -xfd).
| * | | | | | | | | | | | | | | | | Typo in the documentation of cumulativityGravatar Amin Timany2017-08-02
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | | | Unbreak RecTutorial.vGravatar Gaëtan Gilbert2017-08-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The RecTutorial.tex still contains similarly broken Coq code, it just doesn't run it.
| | | | | | | | | | | | | * | | | | Remove old doc/rt files.Gravatar Gaëtan Gilbert2017-08-01
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | | | Add dev/v8-syntax/check-grammar byproducts to gitignore.Gravatar Gaëtan Gilbert2017-08-01
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | | | Remove obsolete filesGravatar Gaëtan Gilbert2017-08-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | db_printers just isn't used. api.txt is superseded by the API OCaml interface.
| | | | | | | | | | | | | * | | | | Add .v extension to dev/doc/notes-on-conversionGravatar Gaëtan Gilbert2017-08-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This gives syntax highlighting in Coq-aware editors.
| | | | | | | | | | | | | * | | | | Remove dev/TODOGravatar Gaëtan Gilbert2017-08-01
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | | | Fix syntax-v8.tex bad parenthesizingGravatar Gaëtan Gilbert2017-08-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Introduced c1e9a27d383688e44ba34ada24fe08151cb5846e
| | | | | | | | | | | | | * | | | | Remove unused Makefiles in dev/tools/Gravatar Gaëtan Gilbert2017-08-01
| |_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | They seem unused since 8f4b7f1 (2007).
| | | | | | | | | | | * | | | | | [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
| |_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied.
| | | | | | | | | | | | | | | * Remove understand_tcc_evars.Gravatar Maxime Dénès2017-08-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Use the functional interface understand_tcc instead.
| | | | | | | | | | | | | | | * Move type_uconstr to Tacinterp.Gravatar Maxime Dénès2017-08-01
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | Have coq-dpdgraph ci test print the differencesGravatar Jason Gross2017-08-01
| |_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows better debugging when it fails.
| | | | | | | | | | | | | | * Remove understand_judgment and understand_judgment_tcc.Gravatar Maxime Dénès2017-08-01
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | * Remove allow_anonymous_refs.Gravatar Maxime Dénès2017-08-01
| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | * Remove pure_open_constr (now open_constr)Gravatar Maxime Dénès2017-08-01
| | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | Printing goals does not evar-normalizes beforehand anymore.Gravatar Pierre-Marie Pédrot2017-08-01
| | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | Detyping functions are now operating on EConstr.t.Gravatar Pierre-Marie Pédrot2017-08-01
| |_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was already the case, but the API was not exposing this.
| | | | | | * | | | | | | | Fix typos. Improve wording.Gravatar Sam Pablo Kuper2017-08-01
| | | | | | | | | | | | | |
| | | | * | | | | | | | | | Improve style slightlyGravatar Sam Pablo Kuper2017-08-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | per @aspiwack's comments in [this pull request review](https://github.com/coq/coq/pull/940).
| | | | | | | | | | | | | * Move glob_constr_ltac_closure to evar_refiner.Gravatar Maxime Dénès2017-08-01
| |_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | |
* | | | | | | | | | | | | Merge PR #933: Fix documentation of Hint Mode (bug #4911).Gravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #932: Fix shuffled documentation.Gravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #929: Add missing paragraph to introductionGravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas).Gravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #926: test-suite uses Extraction TestCompileGravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #925: Document Extraction TestCompileGravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #921: [make] remove compat5 file.Gravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #919: Remove a few useless evar-normalizations in printing code.Gravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #917: Moving --print-version to -print-version for consistency.Gravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #913: Less allocations in DetypingGravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)Gravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #893: Removing default evar-normalization for ARGUMENT EXTEND.Gravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #834: Adding support for recursive notations of the form "x , .. , ↵Gravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | y , z".
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #806: closing bug 5315Gravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.Gravatar Maxime Dénès2017-08-01
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | | | | | | | * | | | | adding a comment to explain the changeGravatar Julien Forest2017-08-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | * | | | | solving b1859Gravatar Julien Forest2017-08-01
| | | | | | | | | | | | | | | | | | | | | | |/ / / / / | | | | | | | | | | | | | | | | | | | | | |/| | | | |
| | | | | | | | | | | | | | | | | | | | * | | | | | | Fix incorrect use of "At the end".Gravatar Sam Pablo Kuper2017-07-31
| | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | * | | | | | | Minor grammar fix: replace a "then" with a "so".Gravatar Sam Pablo Kuper2017-07-31
| | | | | | | | | | | | | | | | | | | | |/ / / / / /
| | | | | | | | | | | | | | | | | | | * / / / / / / Replace jarring use of "Remark" with "Note"Gravatar Sam Pablo Kuper2017-07-31
| | | | | | | | | | | | | | | | | | | |/ / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| | | | | | | | | | | | | | | | * | | | | | | | | Update documentation of cumulativityGravatar Amin Timany2017-07-31
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | * | | | | | | | | Improve errors for cumulativity when monomorphicGravatar Amin Timany2017-07-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We now only issue an error for locally specified (non)cumulativity whenever it is the context (set locally or globally) is monorphic.
| | | | | | | | | | | | | | | | * | | | | | | | | Change the option for cumulativityGravatar Amin Timany2017-07-31
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | * | | | | | | | | Fix typo and Add Jason's example to the docGravatar Amin Timany2017-07-31
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | * | | | | | | | | Improve documentation of cumulativityGravatar Amin Timany2017-07-31
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | * | | | | | | | | Add Jason's example of fun-ext with cumulativityGravatar Amin Timany2017-07-31
| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | * | | | | | | | | Add test for NonCumulative inductivesGravatar Amin Timany2017-07-31
| | | | | | | | | | | | | | | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-18 06:53:20 +0000