| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
|
|
| |
METAIDENT were idents of the form $foobar, only used in quotations.
Note that it removes two dollars in the Coq codebase! Guess I'm absolved
for the $(...) syntax.
|
|\ |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| | |
- Being stricter on the ordinal suffix accepted (only st for 1, 21,
etc, nd for 2, 22, etc., etc.)
- Reporting when the suffix is not the expected one (rather than
considering that, e.g. 2st, is two tokens, a number then an identifier).
|
| | |
|
|/ |
|
| |
|
| |
|
|
|
|
|
| |
I forgot to tell that we are again at the beginning of a line after a
bullet.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The lexer parses bullets only at the beginning of sentence. In
particular, the lexer recognizes sentences (this feature was
introduced for the translator and it is still used for the
beautifier). It recognized "." but not "...'. I added "..." followed
by space or eol as a terminator of sentences. I hope this is
compatible with the rest of the code dealing with end of
sentences.
Fixed also parse_to_dot which was not aware of "...".
Maybe there are similar things to do with coqide or PG?
|
| |
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17047 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
with OCaml 3.12.1).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16754 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
The extended signature is defined in CMap, and should be compatible
with the old one, except that module arguments have to be explicitely
named. The implementation itself is quite unsafe, as it relies on the
current implementation of OCaml maps, even though that should not be
a problem (it has not changed in ages).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16735 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16510 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16448 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
mechanism to retrieve the same information.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16215 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16000 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15969 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15875 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@15818 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
List module. That way, an "open Util" in the header permits using
any function of CList in the List namespace (and in particular, this
permits optimized reimplementations of the List functions, as, for
example, tail-rec implementations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
especially about unused definitions, unused opens and unused rec
flags.
The following patch uses information gathered using these warnings to
clean Coq source tree. In this patch, I focused on warnings whose fix
are very unlikely to introduce bugs.
(a) "unused rec flags". They cannot change the semantics of the program
but only allow the inliner to do a better job.
(b) "unused type definitions". I only removed type definitions that were
given to functors that do not require them. Some type definitions were
used as documentation to obtain better error messages, but were not
ascribed to any definition. I superficially mentioned them in one
arbitrary chosen definition to remove the warning. This is unaesthetic
but I did not find a better way.
(c) "unused for loop index". The following idiom of imperative
programming is used at several places: "for i = 1 to n do
that_side_effect () done". I replaced "i" with "_i" to remove the
warning... but, there is a combinator named "Util.repeat" that
would only cost us a function call while improving readibility.
Should'nt we use it?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
were closed (i.e. the only remaining ones are those of printing/parsing).
Meanwhile, a simplified interface is provided in loc.mli.
This also permits to put Pp in Clib, because it does not depend on
CAMLP4/5 anymore.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15423 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15422 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
+ comment correction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15253 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Signed-off-by: Edward Z. Yang <ezyang@mit.edu>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15148 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14410 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
This way, we forbid contiguous sentences like "tac.{tac.}", which
should now be written with at least 2 spaces: "tac. {tac. }"
This should avoid confusion if a user declare a notation involving
".{" or ".}" as tokens.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14393 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
(an articulating ident needs to be a keyword if the constr entry that
preceeds it is higher than the level of applications).
Also fixed is_ident_not_keyword which only looked at the first letter
and at the keyword status to decide if a token is an ident. This
allowed to simplified define_keywords in Metasyntax.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14389 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
things like (* "forall X : (* Type *), X" *) without warnings
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13971 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
- 8.2 (bug-fix): reverted check for unicode early at notation definition time
(an unsupported "cadratin" space, 0x2003, was used in CoRN!) [by the way,
what to do with unicode spacing characters in general?]
- trunk: improved error message, removed redundant code
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13561 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
on unsupported unicode character) + forbidding unsupported unicode in
Notation declarations too.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13526 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
In particular, the unused lib/tlm.ml and lib/gset.ml are removed
In addition, to simplify code, Libobject.record_object returning only the
('a->obj) function, which is enough almost all the time.
Use Libobject.record_object_full if you really need also the (obj->'a).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The choice between camlp4/5 is done during configure with flags
-usecamlp5 (default for the moment) vs. -usecamlp4.
Currently, to have a full camlp4 compatibility, you need to change
all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI"
into "`EOI" in grammar entries. I've a sed script that does that
(actually the converse), but I prefer to re-think it and check a few
things before branching this sed into the build mechanism.
lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5
and try to propose a common interface (cf LexerSig / GrammarSig).
A few incompatible quotations have been turned into underlying code
manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END
parsable by both camlp4 and 5. See in particular the fate of
<:str_item< declare ... end >>
Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc).
This forces to use camlp5 > 5.01.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
Cf tok.ml, token isn't anymore string*string where first
string encodes the kind of the token, but rather a nice
sum type. Unfortunately, string*string (a.k.a Plexing.pattern)
is still used in some places of Camlp5, so there's a few
conversions back and forth. But the penalty should be quite low,
and having nicer tokens helps in the forthcoming integration
of support for camlp4 post 3.10
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13018 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13016 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13010 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
- A more clever strategy than the use of null spaces (in revision 12058)
for collapsing multi-byte utf-8 characters into one character
(toplevel.ml, 8.3 and trunk only)
- Fixing discard_to_dot in the presence of iterated lexing failures
- Made the lexer state aligned with the start of utf-8 chars instead
of staying in the middle of multi-byte chars when a token is not
recognized (lexer.ml4)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12891 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- This way, the Makefile.build gets shorter and simplier, with a few nasty
hacks removed.
- In particular, we stop creating dummy .ml of .ml4 early "to please ocamldep".
Instead, we now use ocamldep -modules, and process its output via coqdep_boot.
This ways, *.cm* of .ml4 are correctly located, even when some .ml files
aren't generated yet.
- There is no risk of editing the .ml of a .ml4 by mistake, since it is by
default in a binary format (cf pr_o.cmo and variable READABLE_ML4).
M-x next-error still open the right .ml4 at the right location.
- mltop.byteml is now mltop.ml, while mltop.optml keeps its name
- .ml of .ml4 are added to .gitignore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12833 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|