| Commit message (Expand) | Author | Age |
... | |
* | | So as to beautify to work, do not use notations in Inductive types | Hugo Herbelin | 2016-06-16 |
* | | Fixing missing substitution / printing cases of TacSelect. | Pierre-Marie Pédrot | 2016-06-16 |
* | | Fixing printing of keeping hyp on the fly. | Hugo Herbelin | 2016-06-16 |
* | | Fixing printing of inversion as. | Hugo Herbelin | 2016-06-16 |
* | | Fixing extra space in printing destruct/induction as. | Hugo Herbelin | 2016-06-16 |
* | | Fixing printing of induction/destruct as. | Hugo Herbelin | 2016-06-16 |
* | | Fixing printing of pat%constr. | Hugo Herbelin | 2016-06-16 |
* | | A stronger invariant on the syntax of TacAssert, what allows for a | Hugo Herbelin | 2016-06-16 |
* | | Merge PR #79: Let the kernel assume that a (co-)inductive type is positive. | Pierre-Marie Pédrot | 2016-06-16 |
|\ \ |
|
* \ \ | Merge remote-tracking branch 'github/pr/194' into trunk | Maxime Dénès | 2016-06-16 |
|\ \ \ |
|
| | * | | Remove the syntax changes introduced by this branch. | Pierre-Marie Pédrot | 2016-06-15 |
| | * | | Assume totality: dedicated type rather than bool | Arnaud Spiwack | 2016-06-14 |
* | | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-06-09 |
|\ \ \ \
| | |_|/
| |/| | |
|
* | | | | printing.mllib: remove some other .mli-only from a .mllib | Pierre Letouzey | 2016-06-07 |
| | * | | Adding an only printing flag to notations. | Pierre-Marie Pédrot | 2016-06-07 |
| |/ /
|/| | |
|
| * | | Fixing problems introduced in 8.5 with Ltac trace report. E.g. | Hugo Herbelin | 2016-06-06 |
* | | | About printing of traces of failures while calling ltac code. | Hugo Herbelin | 2016-06-06 |
* | | | Removing "rename" from the tactic AST. | Pierre-Marie Pédrot | 2016-06-03 |
* | | | Removing "exact" from the tactic AST. | Pierre-Marie Pédrot | 2016-06-03 |
* | | | Removing "intro" from the tactic AST. | Pierre-Marie Pédrot | 2016-06-03 |
* | | | Removing "double induction" from the tactic AST. | Pierre-Marie Pédrot | 2016-06-03 |
* | | | Move ide serialization libraries from lib/ to ide/ | Emilio Jesus Gallego Arias | 2016-06-02 |
* | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-06-01 |
|\| | |
|
* | | | Feedback cleanup | Emilio Jesus Gallego Arias | 2016-05-31 |
| * | | Pfedit.get_current_context refinement (fix #4523) | Matthieu Sozeau | 2016-05-26 |
* | | | Put the "cofix" tactic in the monad. | Pierre-Marie Pédrot | 2016-05-16 |
* | | | Put the "fix" tactic in the monad. | Pierre-Marie Pédrot | 2016-05-16 |
* | | | Put the "clear" tactic into the monad. | Pierre-Marie Pédrot | 2016-05-16 |
* | | | Actually using the symbol information to print Tactic Notations properly. | Pierre-Marie Pédrot | 2016-05-08 |
* | | | Removing dead code in Pptactic. | Pierre-Marie Pédrot | 2016-05-08 |
* | | | Pass user symbol to tactic notation printers. | Pierre-Marie Pédrot | 2016-05-08 |
* | | | Removing dead code and unused opens. | Pierre-Marie Pédrot | 2016-05-08 |
* | | | Normalizing the names of dynamic types to follow a typ_* scheme. | Pierre-Marie Pédrot | 2016-05-04 |
* | | | Removing useless generic arguments. | Pierre-Marie Pédrot | 2016-05-04 |
* | | | Moving the Val module to Geninterp. | Pierre-Marie Pédrot | 2016-05-04 |
* | | | Switching to an untyped toplevel representation for Ltac values. | Pierre-Marie Pédrot | 2016-05-04 |
* | | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-05-04 |
|\| | |
|
| * | | Remove extraneous space in coqtop/pg output (bug #4675). | Guillaume Melquiond | 2016-05-03 |
* | | | Revert "A heuristic to add parentheses in the presence of rules such as" | Hugo Herbelin | 2016-04-27 |
* | | | Revert "So as to beautify to work, do not use notations in Inductive types" | Hugo Herbelin | 2016-04-27 |
* | | | Revert "In the short term, stronger invariant on the syntax of TacAssert, what" | Hugo Herbelin | 2016-04-27 |
* | | | Revert "Temporary deactivate re-interpretation of terms in beautify." | Hugo Herbelin | 2016-04-27 |
* | | | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and" | Hugo Herbelin | 2016-04-27 |
* | | | Revert "Fixing printing of pat%constr." | Hugo Herbelin | 2016-04-27 |
* | | | Revert "Fixing printing of induction/destruct as." | Hugo Herbelin | 2016-04-27 |
* | | | Revert "Fixing extra space in printing destruct/induction as." | Hugo Herbelin | 2016-04-27 |
* | | | Revert "Fixing printing of inversion as." | Hugo Herbelin | 2016-04-27 |
* | | | Revert "Fixing printing of keeping hyp on the fly." | Hugo Herbelin | 2016-04-27 |
* | | | Revert "Protect printing of intro-patterns from collision when "[|" or "|]"" | Hugo Herbelin | 2016-04-27 |
* | | | Revert "Protect printing of ltac's "context [...]" from possible collision" | Hugo Herbelin | 2016-04-27 |