aboutsummaryrefslogtreecommitdiff
path: root/printing/pptactic.ml
AgeCommit message (Expand)Author
2016-04-27Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Hugo Herbelin
2016-04-27Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Hugo Herbelin
2016-04-27Revert "Fixing printing of induction/destruct as."Hugo Herbelin
2016-04-27Revert "Fixing extra space in printing destruct/induction as."Hugo Herbelin
2016-04-27Revert "Fixing printing of inversion as."Hugo Herbelin
2016-04-27Revert "Fixing printing of keeping hyp on the fly."Hugo Herbelin
2016-04-27Revert "Protect printing of ltac's "context [...]" from possible collision"Hugo Herbelin
2016-04-27Revert "Passing around the precedence to the generic printer so as to solve"Hugo Herbelin
2016-04-27Revert "Temporary hack to restore missing printing of "constr:" in right-hand"Hugo Herbelin
2016-04-27Revert "Taking into account the original grammar rule to print generic"Hugo Herbelin
2016-04-27Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ...Hugo Herbelin
2016-04-27Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Hugo Herbelin
2016-04-27Taking into account the original grammar rule to print genericHugo Herbelin
2016-04-27Temporary hack to restore missing printing of "constr:" in right-handHugo Herbelin
2016-04-27Passing around the precedence to the generic printer so as to solveHugo Herbelin
2016-04-27Protect printing of ltac's "context [...]" from possible collisionHugo Herbelin
2016-04-27Fixing printing of keeping hyp on the fly.Hugo Herbelin
2016-04-27Fixing printing of inversion as.Hugo Herbelin
2016-04-27Fixing extra space in printing destruct/induction as.Hugo Herbelin
2016-04-27Fixing printing of induction/destruct as.Hugo Herbelin
2016-04-27Honor parsing and printing levels for tactic entry in TACTIC EXTEND andHugo Herbelin
2016-04-27In the short term, stronger invariant on the syntax of TacAssert, whatHugo Herbelin
2016-04-27Attempt to slightly improve abusive "Collision between boundHugo Herbelin
2016-04-25Removing dead code related to printing of ML tactics in Pptactic.Pierre-Marie Pédrot
2016-04-12Fixing printing of "destruct in" after ce71ac17268f.Hugo Herbelin
2016-04-11Removing the ad-hoc tactic_expr type.Pierre-Marie Pédrot
2016-04-10Extruding the print_atom primitive.Pierre-Marie Pédrot
2016-04-09Removing extra spaces in printing arguments of VERNAC EXTEND.Hugo Herbelin
2016-04-09Removing automatic printing of leading space in auto_using andHugo Herbelin
2016-04-09In pr_clauses, do not print a leading space by default so that it canHugo Herbelin
2016-04-08Fixing printing of toplevel values.Pierre-Marie Pédrot
2016-04-08Fixing printing of Tactic Notations with tactic arguments.Pierre-Marie Pédrot
2016-03-20Adding a new Ltac generic argument for forced tactics returing unit.Pierre-Marie Pédrot
2016-03-19Removing the untyped representation of genargs.Pierre-Marie Pédrot
2016-03-06Moving Tactic_debug to tactics/ folder.Pierre-Marie Pédrot
2016-03-04Removing the UConstr entry of the tactic_arg AST.Pierre-Marie Pédrot
2016-02-29Moving the "move" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "exists" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "symmetry" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "generalize dependent" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "clearbody" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "clear" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "cofix" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-29Moving the "fix" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2016-02-24Removing the MetaIdArg entry of tactic expressions.Pierre-Marie Pédrot
2016-02-22The tactic generic argument now returns a value rather than a glob_expr.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-17Getting rid of the awkward unpack mechanism from Genarg.Pierre-Marie Pédrot
2016-01-17Temporary commit getting rid of Obj.magic unsafety for Genarg.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-05 14:48:34 +0000