Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | | [location] [ast] Switch Constrexpr AST to an extensible node type. | Emilio Jesus Gallego Arias | 2017-04-25 | |
* | | | | [location] Make location optional in Loc.located | Emilio Jesus Gallego Arias | 2017-04-25 | |
* | | | | [location] Remove Loc.ghost. | Emilio Jesus Gallego Arias | 2017-04-25 | |
* | | | | [location] Use located in misctypes. | Emilio Jesus Gallego Arias | 2017-04-24 | |
* | | | | [location] Use Loc.located for constr_expr. | Emilio Jesus Gallego Arias | 2017-04-24 | |
* | | | | [constrexpr] Make patterns use Loc.located for location information | Emilio Jesus Gallego Arias | 2017-04-24 | |
|/ / / | ||||
* | | | Merge PR#565: Remove VernacError | Maxime Dénès | 2017-04-24 | |
|\ \ \ | ||||
* \ \ \ | Merge PR#580: [ide] Fix #5482 "location for query commands" in IDE. | Maxime Dénès | 2017-04-24 | |
|\ \ \ \ | ||||
| * | | | | [ide] Fix #5482 "location for query commands" in IDE. | Emilio Jesus Gallego Arias | 2017-04-21 | |
| | * | | | Remove VernacError | Gaetan Gilbert | 2017-04-21 | |
| |/ / / | ||||
* | | | | [ide] Set Stateid in query pane. | Emilio Jesus Gallego Arias | 2017-04-20 | |
* | | | | [ide] Rely less on `Stateid.dummy` | Emilio Jesus Gallego Arias | 2017-04-19 | |
|/ / / | ||||
* | | | Merge PR#441: Port Toplevel to the Stm API | Maxime Dénès | 2017-04-12 | |
|\ \ \ | ||||
| * | | | [vernac] vernacentries.mli cleanup | Emilio Jesus Gallego Arias | 2017-04-12 | |
| * | | | [stm] Port the toplevel to the STM. | Emilio Jesus Gallego Arias | 2017-04-12 | |
| * | | | [stm] Move main parsing entry point to the STM. | Emilio Jesus Gallego Arias | 2017-04-12 | |
| * | | | [stm] Remove edit_id. | Emilio Jesus Gallego Arias | 2017-04-12 | |
* | | | | Merge PR#379: Introducing evar-insensitive constrs | Maxime Dénès | 2017-04-11 | |
|\ \ \ \ | ||||
| | | * | | Removing internal support for accepting "{struct x}" and co in "Theorem with". | Hugo Herbelin | 2017-04-09 | |
| | |/ / | ||||
* | / / | [ide] Correctly place warning tags. | Emilio Jesus Gallego Arias | 2017-04-08 | |
| |/ / |/| | | ||||
| * | | Merge branch 'trunk' into pr379 | Maxime Dénès | 2017-04-04 | |
| |\ \ | |/ / |/| | | ||||
* | | | Merge PR#417: No cast surgery in let in | Maxime Dénès | 2017-04-03 | |
|\ \ \ | ||||
* \ \ \ | Merge PR#522: [coqide] Protect against size_allocate race in proofview. | Maxime Dénès | 2017-03-29 | |
|\ \ \ \ | ||||
* | | | | | [ide] Fix typo in pp serialization. | Emilio Jesus Gallego Arias | 2017-03-29 | |
| * | | | | [coqide] Protect against size_allocate race in proofview. | Emilio Jesus Gallego Arias | 2017-03-28 | |
|/ / / / | ||||
| | * | | Merge branch 'trunk' into pr379 | Maxime Dénès | 2017-03-24 | |
| | |\ \ | |_|/ / |/| | | | ||||
| * | | | Replacing "cast surgery" in LetIn by a proper field (see PR #404). | Hugo Herbelin | 2017-03-24 | |
| * | | | Unifying standard "constr_level" names for constructors of local_binder_expr. | Hugo Herbelin | 2017-03-24 | |
| * | | | "Standardizing" the name LocalPatten into LocalRawPattern. | Hugo Herbelin | 2017-03-24 | |
|/ / / | ||||
* | | | make check not CoqIDE-specific | Paul Steckler | 2017-03-22 | |
* | | | [ide protocol] Add comment about leftover parameter. | Emilio Jesus Gallego Arias | 2017-03-21 | |
* | | | [pp] Hide the internal representation of `std_ppcmds`. | Emilio Jesus Gallego Arias | 2017-03-21 | |
* | | | [pp] Fix bug in richpp Format use. | Emilio Jesus Gallego Arias | 2017-03-21 | |
* | | | [xml] Restore protocol compatibility with 8.6. | Emilio Jesus Gallego Arias | 2017-03-21 | |
* | | | [pp] Remove uses of expensive string_of_ppcmds. | Emilio Jesus Gallego Arias | 2017-03-21 | |
* | | | [pp] [ide] Minor cleanups in pp code. | Emilio Jesus Gallego Arias | 2017-03-21 | |
* | | | [pp] Move terminal-specific tagging to the toplevel. | Emilio Jesus Gallego Arias | 2017-03-21 | |
* | | | [pp] Remove special tag type and handler from Pp. | Emilio Jesus Gallego Arias | 2017-03-21 | |
* | | | [ide] Dynamic printing width. | Emilio Jesus Gallego Arias | 2017-03-21 | |
* | | | [ide] richpp clenaup | Emilio Jesus Gallego Arias | 2017-03-21 | |
* | | | [pp] Make feedback the only logging mechanism. | Emilio Jesus Gallego Arias | 2017-03-21 | |
* | | | [pp] Remove unused printing tagging infrastructure. | Emilio Jesus Gallego Arias | 2017-03-21 | |
* | | | [ide] ide_slave doesnt't need to capture stdout | Emilio Jesus Gallego Arias | 2017-03-21 | |
* | | | [ide] Use "log via feedback". | Emilio Jesus Gallego Arias | 2017-03-21 | |
* | | | [safe-string] ide | Emilio Jesus Gallego Arias | 2017-03-14 | |
| * | | Merge branch 'master'. | Pierre-Marie Pédrot | 2017-02-14 | |
| |\ \ | |/ / |/| | | ||||
| * | | Evar-normalizing functions now act on EConstrs. | Pierre-Marie Pédrot | 2017-02-14 | |
| * | | Removing compatibility layers related to printing. | Pierre-Marie Pédrot | 2017-02-14 | |
| * | | Goal API using EConstr. | Pierre-Marie Pédrot | 2017-02-14 | |
* | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-02-01 | |
|\ \ \ | | |/ | |/| |