aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/pptactic.ml
Commit message (Expand)AuthorAge
* Fixing printing of "ltac:" in tactics after surrounding parenthesesGravatar Hugo Herbelin2016-12-02
* Protect printing of ltac's "context [...]" from possible collisionGravatar Hugo Herbelin2016-12-02
* More on fixing #5098 (preserving printing of "in hyp").Gravatar Hugo Herbelin2016-12-02
* Properly parenthesize "ltac:" arguments (bug #5169).Gravatar Guillaume Melquiond2016-11-22
* Fix bug #5098: Symmetry broken in HoTT.Gravatar Pierre-Marie Pédrot2016-10-08
* Addressing OCaml compilation warnings.Gravatar Hugo Herbelin2016-09-16
* Fix bug #4940: Tactic notation printing could be more informative.Gravatar Pierre-Marie Pédrot2016-09-09
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Add and document match, fix and cofix reduction flags.Gravatar Maxime Dénès2016-07-01
* Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
* Adding eintros to respect the e- prefix policy.Gravatar Hugo Herbelin2016-06-18
* Fixing missing substitution / printing cases of TacSelect.Gravatar Pierre-Marie Pédrot2016-06-16
* Fixing printing of keeping hyp on the fly.Gravatar Hugo Herbelin2016-06-16
* Fixing printing of inversion as.Gravatar Hugo Herbelin2016-06-16
* Fixing extra space in printing destruct/induction as.Gravatar Hugo Herbelin2016-06-16
* Fixing printing of induction/destruct as.Gravatar Hugo Herbelin2016-06-16
* A stronger invariant on the syntax of TacAssert, what allows for aGravatar Hugo Herbelin2016-06-16
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-09
|\
| * Fixing problems introduced in 8.5 with Ltac trace report. E.g.Gravatar Hugo Herbelin2016-06-06
* | About printing of traces of failures while calling ltac code.Gravatar Hugo Herbelin2016-06-06
* | Removing "rename" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* | Removing "exact" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* | Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* | Removing "double induction" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* | Actually using the symbol information to print Tactic Notations properly.Gravatar Pierre-Marie Pédrot2016-05-08
* | Removing dead code in Pptactic.Gravatar Pierre-Marie Pédrot2016-05-08
* | Pass user symbol to tactic notation printers.Gravatar Pierre-Marie Pédrot2016-05-08
* | Normalizing the names of dynamic types to follow a typ_* scheme.Gravatar Pierre-Marie Pédrot2016-05-04
* | Removing useless generic arguments.Gravatar Pierre-Marie Pédrot2016-05-04
* | Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
* | Switching to an untyped toplevel representation for Ltac values.Gravatar Pierre-Marie Pédrot2016-05-04
* | Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Gravatar Hugo Herbelin2016-04-27
* | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
* | Revert "Fixing printing of induction/destruct as."Gravatar Hugo Herbelin2016-04-27
* | Revert "Fixing extra space in printing destruct/induction as."Gravatar Hugo Herbelin2016-04-27
* | Revert "Fixing printing of inversion as."Gravatar Hugo Herbelin2016-04-27
* | Revert "Fixing printing of keeping hyp on the fly."Gravatar Hugo Herbelin2016-04-27
* | Revert "Protect printing of ltac's "context [...]" from possible collision"Gravatar Hugo Herbelin2016-04-27
* | Revert "Passing around the precedence to the generic printer so as to solve"Gravatar Hugo Herbelin2016-04-27
* | Revert "Temporary hack to restore missing printing of "constr:" in right-hand"Gravatar Hugo Herbelin2016-04-27
* | Revert "Taking into account the original grammar rule to print generic"Gravatar Hugo Herbelin2016-04-27
* | Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ...Gravatar Hugo Herbelin2016-04-27
* | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
* | Taking into account the original grammar rule to print genericGravatar Hugo Herbelin2016-04-27
* | Temporary hack to restore missing printing of "constr:" in right-handGravatar Hugo Herbelin2016-04-27
* | Passing around the precedence to the generic printer so as to solveGravatar Hugo Herbelin2016-04-27
* | Protect printing of ltac's "context [...]" from possible collisionGravatar Hugo Herbelin2016-04-27
* | Fixing printing of keeping hyp on the fly.Gravatar Hugo Herbelin2016-04-27
* | Fixing printing of inversion as.Gravatar Hugo Herbelin2016-04-27
* | Fixing extra space in printing destruct/induction as.Gravatar Hugo Herbelin2016-04-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 08:52:12 +0000