| Age | Commit message (Collapse) | Author |
|---|
|
And similarly for Haskell: we do not force capitalized/uncapitalized
filenames anymore, but we rather follow the name of the .v file (with
new extensions of course). Ok, this is an incompatible change, but
it is really convenient, some people where actually already doing
some hacks to have this behavior (cf. Compcert).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13260 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- MPbound can be part of visible_mps (when printing the type of
a module parameter, or when printing body of a With), hence
the locality test base_mp mp = base_mp (top_visible_mp ())
isn't accurate.
- new organisation, pp_ocaml_gen is splitted in many sub-functions,
attempt to be clearer
- the shortcut (if List.length ls = 1 then ...) isn't safe,
we might detect name conflict even in this case.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13248 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Add module parameters in the structure of visible_layer,
in order for module params to be part of name clash detection,
avoiding this way a source of potentially wrong code.
- In case of clash, module params are alpha-renamed to something
unique (Foo__XXX where XXX is the number contained in the mbid).
This solves some situations that were unsupported by extraction.
for instance the "Module F (X:T). Module X:=X. ... End F."
- We now check in Coq identifiers the presence of the
extraction-reserved string __. If it is found, we issue a warning
(which might become an error someday).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13240 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13109 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13093 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
For instance:
Extract Inductive nat => int [ "0" "succ" ]
"(fun fO fS n => if n=0 then fO () else fS (n-1))".
See Extraction.v for more details and caveat.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13025 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The command : Extraction Implicit foo [1 3].
will tell the extraction to consider fst and third arg of foo as implicit,
and remove them, unless a final occur-check after extraction shows they
are still there. Here, foo can be a inductive constructor or a global
constant.
This allow typicaly to extract vectors into usual list :-)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12982 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
|
|
1- Management of the name-space in a modular development / sharing of non-logical objects.
2- Performance of atomic module operations (adding a module to the environment, subtyping ...).
1-
There are 3 module constructions which derive equalities on fields from a module to another:
Let P be a module path and foo a field of P
Module M := P.
Module M.
Include P.
...
End M.
Declare Module K : S with Module M := P.
In this 3 cases we don't want to be bothered by the duplication of names.
Of course, M.foo delta reduce to P.foo but many non-logical features of coq
do not work modulo conversion (they use eq_constr or constr_pat object).
To engender a transparent name-space (ie using P.foo or M.foo is the same thing)
we quotient the name-space by the equivalence relation on names induced by the
3 constructions above.
To implement this, the types constant and mutual_inductive are now couples of
kernel_names. The first projection correspond to the name used by the user and the second
projection to the canonical name, for example the internal name of M.foo is
(M.foo,P.foo).
So:
*************************************************************************************
* Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values *
*************************************************************************************
Map and Set indexed on names are ordered on user name for the kernel side
and on canonical name outside. Thus we have sharing of notation, hints... for free
(also for a posteriori declaration of them, ex: a notation on M.foo will be
avaible on P.foo). If you want to use this, use the appropriate compare function
defined in name.ml or libnames.ml.
2-
No more time explosion (i hoppe) when using modules i have re-implemented atomic
module operations so that they are all linear in the size of the module. We also
have no more unique identifier (internal module names) for modules, it is now based
on a section_path like mechanism => we have less substitutions to perform at require,
module closing and subtyping but we pre-compute more information hence if we instanciate
several functors then we have bigger vo.
Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions
above, i will work on it soon...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12406 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(uniformisation of function names, classification). One of the most
visible change is the renaming of section_path into full_path (the
use of name section was obsolete due to the module system, but I
don't know if the new name is the best chosen one - especially it
remains some "sp" here and there).
- Simplification of the interface of classify_object (first argument dropped).
- Simplification of the code for vernac keyword "End".
- Other small cleaning or dead code removal.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12265 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
user contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
|
