index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
printing
/
pptactic.ml
Commit message (
Expand
)
Author
Age
*
still some more dead code removal
letouzey
2012-10-06
*
remove useless hidden_flag in TacMutual(Co)Fix
letouzey
2012-10-06
*
Clean-up : removal of Proof_type.tactic_expr
letouzey
2012-10-06
*
Adding a nominal typing layer to Metasyntax in order to clarify
ppedrot
2012-10-04
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
Added a new tactical infoH tac, that displays the names of hypothesis created...
courtieu
2012-10-01
*
Fixing Show Script issues.
ppedrot
2012-09-20
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
The new ocaml compiler (4.00) has a lot of very cool warnings,
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Getting rid of the undocumented [complete] tactic, which was
ppedrot
2012-07-19
*
The tactic remember now accepts a final eqn:H option (grant wish #2489)
letouzey
2012-07-09
*
induction/destruct : nicer syntax for generating equations (solves #2741)
letouzey
2012-07-09
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
place all pretty-printing files in new dir printing/
letouzey
2012-05-29