index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
intf
/
vernacexpr.mli
Commit message (
Expand
)
Author
Age
...
*
Modulification of identifier
ppedrot
2012-12-14
*
Change [Hints Resolve] to still accept constrs as arguments
msozeau
2012-10-31
*
Fixed #2926:
ppedrot
2012-10-29
*
Change Hint Resolve, Immediate to take a global reference as argument
msozeau
2012-10-26
*
Moved Compat to parsing. This permits to break the dependency of the
ppedrot
2012-10-04
*
Added support for option Local (at module level) in Tactic Notation.
herbelin
2012-08-11
*
Updating headers.
herbelin
2012-08-08
*
A prototype implementation of a Print Namespace command.
aspiwack
2012-07-06
*
Notation: a new annotation "compat 8.x" extending "only parsing"
letouzey
2012-07-05
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr
letouzey
2012-05-29
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
Vernacexpr is now a mli-only file, locality stuff now in locality.ml
letouzey
2012-05-29
[prev]