index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
q_constr.ml4
Commit message (
Expand
)
Author
Age
*
More {raw => glob} changes for consistency
glondu
2010-12-24
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Finish adding out-of-the-box support for camlp4
letouzey
2010-07-09
*
Add (almost) compatibility with camlp4, without breaking support for camlp5
letouzey
2010-05-19
*
static (and shared) camlp4use instead of per-file declaration
letouzey
2010-05-19
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Better handling of the opacity of proof obligations, add the possibility of
msozeau
2008-09-07
*
Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient
herbelin
2008-04-01
*
Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...
msozeau
2007-12-31
*
Generalized CAMLP4USE for pp dependencies
corbinea
2007-07-16
*
Add a parameter to QuestionMark evar kind to say it can be turned into an obl...
msozeau
2007-03-19
*
- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de
herbelin
2006-03-22