aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/pptactic.mli
Commit message (Expand)AuthorAge
* Revert "Taking into account the original grammar rule to print generic"Gravatar Hugo Herbelin2016-04-27
* Taking into account the original grammar rule to print genericGravatar Hugo Herbelin2016-04-27
* Removing dead code related to printing of ML tactics in Pptactic.Gravatar Pierre-Marie Pédrot2016-04-25
* The tactic generic argument now returns a value rather than a glob_expr.Gravatar Pierre-Marie Pédrot2016-02-22
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Tactic notation printing accesses all the token data.Gravatar Pierre-Marie Pédrot2016-01-16
| * rewiring Czar printers that were disabledGravatar Pierre Corbineau2015-03-13
* | rewiring Czar printers that were disabledGravatar Pierre Corbineau2015-03-02
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-02-10
|\|
| * Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* | Splitting ML tactics in one function per grammar entry.Gravatar Pierre-Marie Pédrot2015-01-23
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* Plug the dynamic tags in the Richpp mechanism.Gravatar Pierre-Marie Pédrot2014-11-10
* lib/RichPp: Rename into Richpp.Gravatar Yann Régis-Gianas2014-11-05
* printing/Ppannotation: New annotation for tactic syntactic objects.Gravatar Regis-Gianas2014-11-04
* printing/Pptacticsig: New signature for tactic pretty-printers.Gravatar Regis-Gianas2014-11-04
* Add a interpreted level [tacexpr] to [Tacexpr] together with its printer.Gravatar Arnaud Spiwack2014-11-01
* Qualified ML tactic names. The plugin name is used to discriminateGravatar Pierre-Marie Pédrot2014-07-27
* Removing dead code relative to or_metaid.Gravatar Pierre-Marie Pédrot2014-07-25
* Closing bug #3260Gravatar Julien Forest2014-04-14
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Removing the dependency of every level of tactic ATSs on glob_tactic_expr.Gravatar ppedrot2013-11-10
* Adding genarg printer to debugger.Gravatar ppedrot2013-06-19
* Uniformizing generic argument types.Gravatar ppedrot2013-06-06
* Pptactic.pr_raw_tactic is now without env argumentGravatar letouzey2013-03-14
* Clean-up : removal of Proof_type.tactic_exprGravatar letouzey2012-10-06
* Adding a nominal typing layer to Metasyntax in order to clarifyGravatar ppedrot2012-10-04
* Updating headers.Gravatar herbelin2012-08-08
* place all pretty-printing files in new dir printing/Gravatar letouzey2012-05-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 08:20:49 +0000