aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/pptactic.ml
Commit message (Expand)AuthorAge
* 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
* | Fixing printing of induction/destruct as.Gravatar Hugo Herbelin2016-04-27
* | Honor parsing and printing levels for tactic entry in TACTIC EXTEND andGravatar Hugo Herbelin2016-04-27
* | In the short term, stronger invariant on the syntax of TacAssert, whatGravatar Hugo Herbelin2016-04-27
* | Attempt to slightly improve abusive "Collision between boundGravatar Hugo Herbelin2016-04-27
* | Removing dead code related to printing of ML tactics in Pptactic.Gravatar Pierre-Marie Pédrot2016-04-25
| * Revert "Fixing printing of surrounding parentheses in "ltac:"."Gravatar Hugo Herbelin2016-04-19
| * Fixing printing of surrounding parentheses in "ltac:".Gravatar Hugo Herbelin2016-04-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 15:50:12 +0000