index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
pcoq.mli
Commit message (
Expand
)
Author
Age
...
*
|
ML extensions use untyped representation of user entries.
Pierre-Marie Pédrot
2016-01-17
*
|
Removing the special status of open_constr generic argument.
Pierre-Marie Pédrot
2015-12-28
*
|
CLEANUP: Vernacexpr.VernacDeclareTacticDefinition
Matej Kosik
2015-12-18
*
|
Adding a token "index" representing positions (1st, 2nd, etc.).
Hugo Herbelin
2015-12-15
*
|
Fixing the return type of the Atoken symbol.
Pierre-Marie Pédrot
2015-10-28
*
|
Removing unused code in Pcoq.
Pierre-Marie Pédrot
2015-10-27
*
|
Finer type for Pcoq.interp_entry_name.
Pierre-Marie Pédrot
2015-10-27
*
|
Indexing existentially quantified entries returned by interp_entry_name.
Pierre-Marie Pédrot
2015-10-27
*
|
Type-safe grammar extensions.
Pierre-Marie Pédrot
2015-10-27
*
|
Pcoq entries are given a proper module.
Pierre-Marie Pédrot
2015-10-26
*
|
Getting rid of the Atactic entry.
Pierre-Marie Pédrot
2015-10-25
*
|
Getting rid of the Agram entry.
Pierre-Marie Pédrot
2015-10-25
*
|
Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.
Pierre-Marie Pédrot
2015-10-21
*
|
Expliciting some uses of Compat module.
Pierre-Marie Pédrot
2015-10-21
|
/
*
grammar: export constr_eval
Enrico Tassi
2015-03-30
*
grammar: export hypident
Enrico Tassi
2015-03-30
*
Update headers.
Maxime Dénès
2015-01-12
*
Fixing bugs #3723 and #3787 (reinitialization of camlp5 empty levels)
Hugo Herbelin
2014-11-06
*
Adding a new intro-pattern for "apply in" on the fly. Using syntax
Hugo Herbelin
2014-08-18
*
Moving the TacExtend node from atomic to plain tactics.
Pierre-Marie Pédrot
2014-08-18
*
Properly declare uconstr as an argument for TACTIC EXTEND.
Arnaud Spiwack
2014-08-05
*
Removing useless use of metaids in tactic AST.
Pierre-Marie Pédrot
2014-05-22
*
Adding way to get the list of the accepted tactic notation arguments.
Pierre-Marie Pédrot
2014-05-17
*
Closing bug #3260
Julien Forest
2014-04-14
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Removing non-marshallable data from the Agram constructor. Instead of
Pierre-Marie Pédrot
2014-02-16
*
Getting rid of casted_open_constr. It was only used by the
Pierre-Marie Pédrot
2013-11-30
*
Dir_path --> DirPath
letouzey
2013-02-19
*
Modulification of name
ppedrot
2012-12-18
*
Modulification of dir_path
ppedrot
2012-12-14
*
Modulification of identifier
ppedrot
2012-12-14
*
Moved Compat to parsing. This permits to break the dependency of the
ppedrot
2012-10-04
*
Updating headers.
herbelin
2012-08-08
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
remove many excessive open Util & Errors in mli's
letouzey
2012-05-29
*
Migrate the grammar entry about "Ltac" into g_vernac.ml4.
letouzey
2012-05-29
*
New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr
letouzey
2012-05-29
*
Glob_term now mli-only, operations now in Glob_ops
letouzey
2012-05-29
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
Noise for nothing
pboutill
2012-03-02
*
Reverted previous commit, which broke library compilation.
ppedrot
2012-01-20
*
This is a quick hack to permit the parsing of the locality flag in the Progra...
ppedrot
2012-01-20
*
More {raw => glob} changes for consistency
glondu
2010-12-24
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Extension of the recursive notations mechanism
herbelin
2010-07-22
*
Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).
herbelin
2010-07-22
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Using vernac parsing for Function
jforest
2010-06-08
[prev]
[next]