index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
printing
/
pptactic.mli
Age
Commit message (
Expand
)
Author
2016-05-08
Pass user symbol to tactic notation printers.
Pierre-Marie Pédrot
2016-05-04
Moving the Val module to Geninterp.
Pierre-Marie Pédrot
2016-04-27
Revert "Taking into account the original grammar rule to print generic"
Hugo Herbelin
2016-04-27
Taking into account the original grammar rule to print generic
Hugo Herbelin
2016-04-25
Removing dead code related to printing of ML tactics in Pptactic.
Pierre-Marie Pédrot
2016-02-22
The tactic generic argument now returns a value rather than a glob_expr.
Pierre-Marie Pédrot
2016-01-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2016-01-16
Tactic notation printing accesses all the token data.
Pierre-Marie Pédrot
2015-03-13
rewiring Czar printers that were disabled
Pierre Corbineau
2015-03-02
rewiring Czar printers that were disabled
Pierre Corbineau
2015-02-10
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-02-02
Removing dead code.
Pierre-Marie Pédrot
2015-01-23
Splitting ML tactics in one function per grammar entry.
Pierre-Marie Pédrot
2015-01-12
Update headers.
Maxime Dénès
2014-11-10
Plug the dynamic tags in the Richpp mechanism.
Pierre-Marie Pédrot
2014-11-05
lib/RichPp: Rename into Richpp.
Yann Régis-Gianas
2014-11-04
printing/Ppannotation: New annotation for tactic syntactic objects.
Regis-Gianas
2014-11-04
printing/Pptacticsig: New signature for tactic pretty-printers.
Regis-Gianas
2014-11-01
Add a interpreted level [tacexpr] to [Tacexpr] together with its printer.
Arnaud Spiwack
2014-07-27
Qualified ML tactic names. The plugin name is used to discriminate
Pierre-Marie Pédrot
2014-07-25
Removing dead code relative to or_metaid.
Pierre-Marie Pédrot
2014-04-14
Closing bug #3260
Julien Forest
2014-03-05
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2013-11-10
Removing the dependency of every level of tactic ATSs on glob_tactic_expr.
ppedrot
2013-06-19
Adding genarg printer to debugger.
ppedrot
2013-06-06
Uniformizing generic argument types.
ppedrot
2013-03-14
Pptactic.pr_raw_tactic is now without env argument
letouzey
2012-10-06
Clean-up : removal of Proof_type.tactic_expr
letouzey
2012-10-04
Adding a nominal typing layer to Metasyntax in order to clarify
ppedrot
2012-08-08
Updating headers.
herbelin
2012-05-29
place all pretty-printing files in new dir printing/
letouzey
