index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
grammar
/
q_coqast.ml4
Commit message (
Expand
)
Author
Age
*
Dir_path --> DirPath
letouzey
2013-02-19
*
New implementation of the conversion test, using normalization by evaluation to
mdenes
2013-01-22
*
Yet a new reduction tactic in Coq : cbn
pboutill
2012-12-21
*
Modulification of dir_path
ppedrot
2012-12-14
*
Modulification of identifier
ppedrot
2012-12-14
*
remove useless hidden_flag in TacMutual(Co)Fix
letouzey
2012-10-06
*
Moved Compat to parsing. This permits to break the dependency of the
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
*
The new ocaml compiler (4.00) has a lot of very cool warnings,
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
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 files specific to camlp4 syntax extensions in grammar/
letouzey
2012-05-29