index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
grammar
Commit message (
Expand
)
Author
Age
*
More monomorphizations
ppedrot
2012-11-13
*
Added a CString module.
ppedrot
2012-11-13
*
Added an Int module with dummy utility functions.
ppedrot
2012-11-08
*
Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp
letouzey
2012-10-16
*
Continue killing hidden tactics : no more generated h_xxx
letouzey
2012-10-15
*
Stylistic improvement: avoid a "if match List.hd"
letouzey
2012-10-15
*
remove useless hidden_flag in TacMutual(Co)Fix
letouzey
2012-10-06
*
remove Refiner.abstract_tactic and similar
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
*
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
*
Argextend: avoid useless "open Extrawit"
letouzey
2012-10-02
*
Added a new tactical infoH tac, that displays the names of hypothesis created...
courtieu
2012-10-01
*
Reusing the Hashset data structure in Hashcons. Hopefully, this should
ppedrot
2012-09-26
*
More cleanup of Util: utf8 aspects moved to a new file unicode.ml
letouzey
2012-09-18
*
As r15801: putting everything from Util.array_* to CArray.*.
ppedrot
2012-09-14
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
The new ocaml compiler (4.00) has a lot of very cool warnings,
regisgia
2012-09-14
*
Made Pp.std_ppcmds opaque.
ppedrot
2012-09-13
*
Updating headers.
herbelin
2012-08-08
*
Better exception handling in TACTIC EXTEND and VERNAC EXTEND (fix #2797)
letouzey
2012-07-12
*
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
*
More cleaning
ppedrot
2012-06-01
*
Extend become a mli-only file in intf/
letouzey
2012-05-29
*
place all files specific to camlp4 syntax extensions in grammar/
letouzey
2012-05-29