| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
| |
syntax constr:foo and ipattern:bar (which is not very nice for
parsing, b.t.w.).
Now one is able to dynamically add quotations of the form name:...
that will use the provided function to create a dynamically typed
argument.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16611 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
Ok, this is merely a matter of taste, but up to now the usage
in Coq is rather to use capital letters instead of _ in the
names of inner modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
things up. Records are used instead of their equivalents as tuples.
This is maybe syntactically heavier, but this is semantically
equivalent and easier to understand.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15848 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
| |
kernel on CAMLP4/5 structures, and consequently should also erase
such structures from vo files.
This modification requires some code duplication, mainly while
reimplementing our own location data type. This is chiefly visible
in the ml4 files, where CAMLP4/5 locations must be manually converted
to our locations with an explicit (!@) cast operator.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15847 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
Two gains:
- no Summary in Grammar.cma
- get rid of the hack concerning error_invalid_pattern_notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15386 85f007b7-540e-0410-9357-904b9bb8a0f7
|
ppedrot
letouzey
herbelin