index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
printing
/
pptacticsig.mli
Age
Commit message (
Expand
)
Author
2016-09-15
Moving Ltac printers to ltac/ folder.
Pierre-Marie Pédrot
2016-09-08
Unplugging Pptactic from Ppvernac.
Pierre-Marie Pédrot
2016-06-09
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-06
Fixing problems introduced in 8.5 with Ltac trace report. E.g.
Hugo Herbelin
2016-06-06
About printing of traces of failures while calling ltac code.
Hugo Herbelin
2016-05-08
Removing dead code in Pptactic.
Pierre-Marie Pédrot
2016-05-04
Moving the Val module to Geninterp.
Pierre-Marie Pédrot
2016-04-27
Revert "Passing around the precedence to the generic printer so as to solve"
Hugo Herbelin
2016-04-27
Passing around the precedence to the generic printer so as to solve
Hugo Herbelin
2016-04-11
Removing the ad-hoc tactic_expr type.
Pierre-Marie Pédrot
2016-04-08
Fixing printing of toplevel values.
Pierre-Marie Pédrot
2016-03-06
Moving Tactic_debug to tactics/ folder.
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-02
Reduce dependencies of interface files.
Guillaume Melquiond
2015-12-30
External tactics and notations now accept any tactic argument.
Pierre-Marie Pédrot
2015-12-21
Using dynamic values in tactic evaluation.
Pierre-Marie Pédrot
2015-12-18
Tying the loop in tactic printing API.
Pierre-Marie Pédrot
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-17
Moving printing code for red_expr and may_eval to Pptactic.
Pierre-Marie Pédrot
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
