| Age | Commit message (Collapse) | Author |
|---|
|
user contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(diff says it's a big commit, whereas diff -w says it's an empty one ;-)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11547 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
for debug / external output via coqtop.byte + Drop
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10895 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Initial Idea: getting rid of nasty renaming issues in modules, in
particular bugs #820 (part d) #1340 #1526 #1654
Final effect: lots of changes, simplifications, cleanups, unrelated
fixes and ehancements, and also probably some regressions (time will
tell).
A few details:
* no more experimental "Toplevel" language.
* no more functors Make in Ocaml/Haskell/Scheme. The spirit of these
functors and Mlpp_params was already not followed much, and this
framework was more a nuisance that anything else.
* instead, some records language_descr regrouping the specific
features of the different output languages.
* Common now comes before Ocaml/Haskell/Scheme, these ones are now
independant from each others. print_structure_to_file is now
in Extract_env.
* A nice detail: no more duplications of warnings concerning axioms.
* In modular extraction, the clashes due to the opened modules
are now computed once and for all thanks to record_contents_fstlev,
instead of re-asking Coq each time about these opened modules and
using Extraction.constant_kind
* some utilities about modules_path added and/or moved from Modutil
to Table.
* using a .v file as a module, e.g. in a functor application should
now works in modular extraction.
Now concerning renaming issues themselves:
* printing is done twice, the first time toward /dev/null, in order
to encounter the naming issues unsolvable by a simple qualification.
On the second run, we create artificial modules Coq__123 for
allowing qualification of these hidden objects.
* names are now fully separated into their syntaxic categories:
terms/types/constructors/modules
* Only one last unsupported situation (but at least detected and
signaled by an error): an object M.t from an external file-module
M.v can't be printed when a local module M is in the way.
This situation is really unlikely (in Coq you must use _long_
file-module name, e.g. Init.Datatypes.nat). It could be solved
by inserting "module Coq_123 = M" at the beginning of the file,
but then the signature of Coq_123 (that is, the one of M) should
be written explicitely in the .mli, which is _really_ not nice.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10232 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4847 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4843 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
------------------
- (Recursive) Extraction Module devient (Recursive) Extraction Library
(pour cause d'ambiguite avec les nouveaux modules Coq).
- un nouveau Extraction Module qui extrait dans le toplevel tout module Coq
- tout fixpoint est de nouveau inlinable (Yves).
- fix bug du calcul d'env minimal des modules en extraction monolithique.
- un nouveau fichier Modutil regroupant manques de Modops & functions
specifiques aux modules MiniML
- plus d'aliases a trainer (mais des substitutions des le depart)
- ET SURTOUT: un nommage correct (ou du moins moins pire) dans les modtypes
et les functors.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3934 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3569 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3432 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3380 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t"
- "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième
pretty-printer dans ppconstr.ml est basé sur "constr_expr".
- Nouveau répertoire "interp" qui hérite de la partie interprétation qui
se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml;
constrextern.ml est l'équivalent de termast.ml pour le nouveau
printer; topconstr.ml; contient la définition de "constr_expr";
modintern.ml remplace astmod.ml)
- Libnames.reference tend à remplacer Libnames.qualid
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
* extraction.ml + modulaire (cf extract_type) et + proche theorie (cf feu extract_app)
* table.ml filtre les Extract Constant vers types ou terms
* extract_env.ml refuse maintenant les Extraction constr.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2886 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
commandes vernaculaires (cf dev/changements.txt pour plus de précisions)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
documentation code
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1528 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1498 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1493 85f007b7-540e-0410-9357-904b9bb8a0f7
|
