| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-08-02 | Makefile: 'make clean' now immune to the check for binary files without sources | Pierre Letouzey | |
| 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). | |||
| 2017-08-02 | Properly classifying Ltac2 notations. | Pierre-Marie Pédrot | |
| 2017-08-02 | Fixing parsing of match branches. | Pierre-Marie Pédrot | |
| 2017-08-02 | Removing deprecated stuff. | Pierre-Marie Pédrot | |
| 2017-08-02 | Typo in the documentation of cumulativity | Amin Timany | |
| 2017-08-02 | Adding a few standard notations for Ltac1 tactics. | Pierre-Marie Pédrot | |
| 2017-08-02 | Bindings use open constr quotations. | Pierre-Marie Pédrot | |
| 2017-08-02 | Adding the open_constr scope | Pierre-Marie Pédrot | |
| 2017-08-02 | Better test Makefile. | Pierre-Marie Pédrot | |
| 2017-08-02 | Tentatively fixing a few parsing issues. | Pierre-Marie Pédrot | |
| 2017-08-02 | Fixup reification of egeneralize. | Pierre-Marie Pédrot | |
| 2017-08-01 | More primitive tactics. | Pierre-Marie Pédrot | |
| 2017-08-01 | Expanding unification variables in typechecking error messages. | Pierre-Marie Pédrot | |
| 2017-08-01 | Don't reuse Coq AST for binding quotations. | Pierre-Marie Pédrot | |
| This allows antiquotations in binding lists. | |||
| 2017-08-01 | Fix parsing of fresh ident antiquotations. | Pierre-Marie Pédrot | |
| 2017-08-01 | Introducing the all-mighty intro-patterns. | Pierre-Marie Pédrot | |
| 2017-08-01 | Unbreak RecTutorial.v | Gaëtan Gilbert | |
| The RecTutorial.tex still contains similarly broken Coq code, it just doesn't run it. | |||
| 2017-08-01 | Remove old doc/rt files. | Gaëtan Gilbert | |
| 2017-08-01 | Add dev/v8-syntax/check-grammar byproducts to gitignore. | Gaëtan Gilbert | |
| 2017-08-01 | Remove obsolete files | Gaëtan Gilbert | |
| db_printers just isn't used. api.txt is superseded by the API OCaml interface. | |||
| 2017-08-01 | Add .v extension to dev/doc/notes-on-conversion | Gaëtan Gilbert | |
| This gives syntax highlighting in Coq-aware editors. | |||
| 2017-08-01 | Remove dev/TODO | Gaëtan Gilbert | |
| 2017-08-01 | Fix syntax-v8.tex bad parenthesizing | Gaëtan Gilbert | |
| Introduced c1e9a27d383688e44ba34ada24fe08151cb5846e | |||
| 2017-08-01 | Remove unused Makefiles in dev/tools/ | Gaëtan Gilbert | |
| They seem unused since 8f4b7f1 (2007). | |||
| 2017-08-01 | [flags] Remove XML output flag. | Emilio Jesus Gallego Arias | |
| 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. | |||
| 2017-08-01 | Remove understand_tcc_evars. | Maxime Dénès | |
| Use the functional interface understand_tcc instead. | |||
| 2017-08-01 | Move type_uconstr to Tacinterp. | Maxime Dénès | |
| 2017-08-01 | Have coq-dpdgraph ci test print the differences | Jason Gross | |
| This allows better debugging when it fails. | |||
| 2017-08-01 | Remove understand_judgment and understand_judgment_tcc. | Maxime Dénès | |
| 2017-08-01 | Remove allow_anonymous_refs. | Maxime Dénès | |
| 2017-08-01 | Remove pure_open_constr (now open_constr) | Maxime Dénès | |
| 2017-08-01 | Fix documentation. | Pierre-Marie Pédrot | |
| 2017-08-01 | Printing goals does not evar-normalizes beforehand anymore. | Pierre-Marie Pédrot | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |