| Commit message (Collapse) | Author | Age |
... | |
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13820 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
As said in CHANGES:
<<
The inlining done during application of functors can now be controlled
more precisely. In addition to the "!F G" syntax preventing any inlining,
we can now use a priority level to select parameters to inline :
"<30>F G" means "only inline in F the parameters whose levels are <= 30".
The level of a parameter can be fixed by "Parameter Inline(30) foo".
When levels aren't given, the default value is 100. One can also use
the flag "Set Inline Level ..." to set a level.
>>
Nota : the syntax "Parameter Inline(30) foo" is equivalent to
"Set Inline Level 30. Parameter Inline foo.",
and "Include <30>F G" is equivalent to "Set Inline Level 30. Include F G."
For instance, in ZBinary, eq is @Logic.eq and should rather be inlined,
while in BigZ, eq is (fun x y => [x]=[y]) and should rather not be inlined.
We could achieve this behavior by setting a level such as 30 to the
parameter eq, and then tweaking the current level when applying functors.
This idea of levels might be too restrictive, we'll see, but at least
the implementation of this change was quite simple. There might be
situation where parameters cannot be linearly ordered according to their
"inlinablility". For these cases, we would need to mention names to inline
or not at a functor application, and this is a bit more tricky
(and might be a pain to use if there are many names).
No documentation for the moment, since this feature is experimental
and might still evolve.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13807 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
According to B. Gregoire, this stuff is obsolete. Fine control
on when to launch the VM in conversion problems is now provided
by VMcast. We were already almost never boxing definitions anymore
in stdlib files.
"(Un)Boxed Definition foo" will now trigger a parsing error,
same with Fixpoint. The option "(Un)Set Boxed Definitions"
aren't there anymore, but tolerated (as no-ops), since unknown
options raise a warning instead of an error by default.
Some more cleaning could be done in the vm.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13806 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13783 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
- renamed load_object in mltop into load_ml_object to avoid confusion
with load_object in library
- flushed the liboject warning in real time
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13596 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
discharge bug of implicit arguments related to commit 13484 (multiple
implicit arguments sequences patch).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13500 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
- fixing r13483 (supposed dead code in impargs was actually half-living:
implicit arguments mode should merge with the {...} manually given
implicit arguments but not with the "Implicit Arguments [...]" arguments),
- fixing code of drop_first_implicits in r13484.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13490 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
Example: "Implicit Arguments eq_refl [[A] [x]] [[A]]".
This should a priori be used with care (it might be a bit disturbing
seeing the same constant used with apparently incompatible signatures).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13484 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
automatic and manual implicit arguments twice).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13483 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13469 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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
too late, in a global environment which was no longer the correct one,
leading to the failure of error printing (hence an anomaly) in case
the command modified the state in several steps.
Now, errors raised by vernac commands are processed in the same
(intermediate) state they were raised from, just before rolling back
to the original state.
that modify the state in several
Now, errors raised by vernac commands that modify the state in several
steps (say S1, S2, ..., Sn) are processed in the state they were
produced in (S1, S2, ... Sn-1),
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13431 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(declare_constant_gen was not exported, leading to a lot of silly tests
before calling those functions) and replaced them by
declare_constant : ?internal:internal_flat -> ...
declare_constant's default behaviour is the same as the old declare_constant.
* fixed the default behaviour of inductive scheme failure during coq's
compilation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13395 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13382 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13381 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
proofs is now the default behavior of coqtop.
* lib/Coqtop: Update accordingly.
* checker/Check library/Library:
Pass the right "load_proofs" flag to LightenLibrary.load.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13379 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13378 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
This module introduces an indirection behind opaque const_body
to enable the optional demarshalling of them.
* library/Library checker/Check: Use LightenLibrary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13377 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13376 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13375 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
- Moved Global Set from Keep to Substitute to ensure it is activated
in real time and not only after the main parts of the module
- Renamed Importation into Import in option name
- Made "Print Libraries" prints the modules in the importation order
(which is the most relevant order for non-commutative declarations)
instead of load order
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13318 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
a 3 state type to allow:
* KernelVerbose / KernelSilent : handle the display of messages launch by Coq
* UserVerbose : handle the display of messages launch by user actions
Coq will still behaves the same way (TODOs in the code mark the places
where we can now change the behaviour). I'll remove them in a few days
when we'll have agreed on the correct behaviour.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13217 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
improve compatibility between Coq versions).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13196 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Applied it to fix mli file headers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13175 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13119 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13067 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
|
|
|
|
|
|
|
| |
Including a module or module type into the top module.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12994 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
dev/ocamldoc/
old "make source-doc" that documents ml files and didn't work is now
"make ml-doc" but still don't work :-)
"make clean" cleans dev/ocamldoc/ properly
wierd? calls of dependency graph generation leave unchanged
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12978 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12976 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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
dev/ocamlweb-doc has been erased. I hope no one still use the
"new-parse" it generate.
In dev/,
make html will generate in dev/html/ "clickable version of mlis". (as
the caml standard library)
make coq.pdf will generate nearly the same awfull stuff that coq.ps was.
make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of
the given directory.
ocamldoc comment syntax is here :
http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html
The possibility to put graphs in pdf/html seems to be lost.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
so that we can return the right error message when trying to
declare a scheme twice.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12965 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12939 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Simplified in passing generation of names for the "Goal" command.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12910 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- make links to section variables working (used qualified names for
disambiguation and fixed the place in intern_var where to dump them)
(wish #2277)
- mapping of physical to logical paths now follows coq (see bug #2274)
(incidentally, it was also incorrectly seeing foobar.v as a in directory foo)
- added links for notations
- added new category "other" for indexing entries not starting with latin letter
(e.g. notations or non-latin identifiers which was otherwise broken)
- protected non-notation strings (from String.v) from utf8 symbol interpretation
- incidentally quoted parseable _ in notations to avoid confusion with
placeholder in the "_ + _" form of notation
- improved several "Sys_error" error messages
- fixed old bug about second dot of ".." being interpreted as regular dot
- removed obsolete lexer in index.mll (and renamed index.mll to index.ml)
- added a test-suite file for testing various features of coqdoc
Things that still do not work:
- when a notation is redefined several times in the same scope, only
the link to the first definition works
- if chars and symbols are not separated in advance, idents
that immediately follow symbols are not detected
(e.g. as in {True}+{True} where coqdoc sees a symbol "+{True}")
- parentheses, curly brackets and semi-colon not linked in notations
Things that can probably be improved:
- all notations are indexed in the same category "other"; can we do better?
- all non-latin identifiers (e.g. Greek letters) are also indexed in the
same "other" category; can we do better?
- globalization data for notations could be compacted (currently there is one
line per each proper location covered by the notation)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12890 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
As we can now jump right onto a closed segment, there is no need for
complicated pattern matching.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12758 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
You can now BackTo directly inside segments
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12757 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12706 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
- Include Self and equivalence of names
- Include type in modules and nametab
- Bang operator and composition of substitution
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12682 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
For F(X:T), the application !F M works as F M, except that if module type T
contains some "Inline" annotations, they are not taken in account when substituting
X with M in F. See forthcoming commits for examples of use for this feature.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12678 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Syntax Include Type is still active, but deprecated, and triggers a warning.
The syntax M <+ M' <+ M'', which performs internally an Include, also
benefits from this: M, M', M'' can be independantly modules or module type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12640 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12569 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
functors
For Module F(X:SIG), making now a Include F will try to find the X fields in
the current context, just as was doing earlier Include Self F. This specific
syntax is removed, freeing the keyword "Self". Anyway, with the use of the
syntax "<+" there was already hardly any need for syntax "Include Self".
Idem for Include Type.
Beware that a typo such as "Include F" instead of "Include F G" will
produce a different message now, about a missing field instead of
a not-enough-applied functor.
By the way, some code clean-up and factorisation of inner recursive
functions in declaremods.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12566 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
mod_subst <--- Some inlining informations was propagated into module implementation whereas those informations should stay in module type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12558 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- backtrack on incompatibility introduced in intro while trying to
simplify the condition about when to restart the subscript of a name
(the legacy says: find a new name from x0 if the name xN exists in
the context but find a new name from xN+1 if the name xN does not
exists in the context but is a global to avoid).
- made the names chosen by "intro" compliant with the ones printed in
the goal and used for "intros until" (possible source of rare
incompatibilities) [replaced the use of visibly_occur_id for
printing the goal into a call to next_name_away_in_goal]
- also made the names internal to T in "T -> U" printed the same in
the goal as they are while printing T after it is introducted in the
hypotheses [non contravariant propagation of boolean isgoal in
detype_binder]
- simplified a bit visibly_occur_id (the Rel and Var cases were useless as
soon as the avoid list contained the current env); still this function is
costly with polynomial time in the depth of binders
- see file output/Naming.v for examples
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12549 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
NZAddPropFunct in NZAdd.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12535 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
Any place where <: was legal can now contain many <: declarations.
Moreover we can say that the module type we are declaring is a subtype
of an earlier module type. See DecidableType2 for examples.
Also try to handle correctly the freeze/unfreeze summaries
when simulating start/include/end (syntax ... := ... <+ ...)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12532 85f007b7-540e-0410-9357-904b9bb8a0f7
|