index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
pcoq.ml4
Commit message (
Expand
)
Author
Age
*
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
*
Properly declare uconstr as an argument for TACTIC EXTEND.
Arnaud Spiwack
2014-08-05
*
Fixing #3390 (mismatch simple_tactic/tactic0 leading to segfault).
Hugo Herbelin
2014-06-21
*
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
*
Removing the useless pattern ident genarg.
Pierre-Marie Pédrot
2013-12-19
*
Getting rid of casted_open_constr. It was only used by the
Pierre-Marie Pédrot
2013-11-30
*
Removing a bunch of generic equalities.
ppedrot
2013-09-27
*
Expurgating the useless difference between List0 and List1 at the
ppedrot
2013-07-05
*
Removing the use of leveled tactics wit_tacticn. It is now handled
ppedrot
2013-07-02
*
Cutting the dependency of Genarg in constr_expr, glob_constr
ppedrot
2013-06-21
*
Proof-of-concept: moved four easy-to-handle generic arguments to
ppedrot
2013-06-18
*
Uniformizing generic argument types.
ppedrot
2013-06-06
*
avoid (Int.equal (cmp ...) 0) when a boolean equality exists
letouzey
2013-02-19
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Monomorphization (parsing)
ppedrot
2012-11-25
*
More monomorphizations
ppedrot
2012-11-13
*
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
*
More cleaning on Utils and CList. Some parts of the code being
ppedrot
2012-09-17
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Two adaptations after the changes of level of ->
letouzey
2012-07-06
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
Migrate the grammar entry about "Ltac" into g_vernac.ml4.
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
*
Oversight in revision 14292.
pboutill
2011-07-27
*
Pcoq.ml4: fix a typo in a comment to please ocamldoc
letouzey
2011-04-26
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
adapt slighlty r13642 to support both camlp4 and camlp5-5 and camlp5-6
letouzey
2010-11-18
*
Support for camlp5 6.02.0 (Closes: #2432)
glondu
2010-11-16
*
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
*
Using vernac parsing for Function
jforest
2010-06-08
*
Add (almost) compatibility with camlp4, without breaking support for camlp5
letouzey
2010-05-19
*
Nicer representation of tokens, more independant of camlp*
letouzey
2010-05-19
*
static (and shared) camlp4use instead of per-file declaration
letouzey
2010-05-19
*
Discontinue support for ocaml 3.09.*
letouzey
2010-05-19
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2010-04-22
*
Several bug-fixes and improvements of coqdoc
herbelin
2010-03-29
[next]