| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11873 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
of the archive to install in coq user-contrib installation directory.
- Relaxed the validity check on identifiers from an error to a warning.
- Added a filtering option to Print LoadPath.
- Support for empty root in option -R.
- Better handling of redundant paths in ml loadpath.
- Makefile's: Added target initplugins and added initplugins to coqbinaries.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11713 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
for record fields (using "someproj : sometype where not := constr" syntax). Only one
notation allowed currently and no redeclaration after the record
declaration either (will be done for typeclasses).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11542 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Option -R fait maintenant des Import à tous les niveaux de la
hiérarchie de répertoires. Par exemple, Require "Init.Wf" marche.
- Option -I rend maintenant possible l'accès aux sous-répertoires via
les noms qualifiés. Ainsi -R est exactement comme -I sauf qu'il
rend récursivement visibles les noms non qualifiés.
- Ajout option -I dir -as coqdir, et par symétrie, -R dir -as coqdir.
- Ajout option -exclude-dir pour exclure certains sous-répertoires de
la descente récursive de -R.
- Amélioration message de localisation pour fichiers venant d'un "state".
- Adaptation du checker (et ajout du test check_coq_overwriting qui
semblait involontairement oublié dans l'option -R).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11188 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
- New vernac command "Delete"
- New vernac command "Undo To"
- Added a few hooks used by new contrib/interface
- Beta/incomplete version of dependency generation and dumping
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10580 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10308 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Au passage, un peu plus de standardisation des noms de fonctions de
globalisation
Principe de base :
locate_foo : qualid -> foo (échoue avec Not_found)
global : reference -> global_reference (échoue avec UserError)
global_of_foo : foo -> global_reference (échoue avec UserError)
f_with_alias : se comporte comme f mais prenant aussi en compte les
notations de la forme "Notation id:=ref"
Principale exception :
locate, au lieu de locate_global
locate_global_with_alias, qui prend en entrée un "qualid located"
Restent beaucoup de fonctions qui pourraient utiliser
global_with_alias au lieu de global, notamment dans contribs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10305 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
discharge_function des implicites au cas des scopes d'arguments)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9475 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Avant : une unique méthode discharge_function qui avait accès à l'ancien
environnement mais pas de possibilité de raisonner avec les objets
du nouvel environnement en cours de construction. C'était problématique
pour le discharge des implicites, arguments scope, etc qui étaient
finalement faits en même temps que le discharge des constantes et inductifs
mais avec pour effets de bord que les entrées dans la lib_stk arrivaient
juste avant celles des constantes et inductifs avec des problèmes pour
effacer les bonnes entrées au moment du reset
- Maintenant : deux méthodes distinctes : discharge_function qui est appliquée
pour collecter de l'ancien environnement ce qui est à garder dans la
section et rebuild_function qui reconstruit le nouvel environnement
connaissant déjà les nouvelles valeurs des objets précédants (on se rapproche
ainsi plus de la méthode en deux temps d'avant la 8.1 tout en offrant
l'extensibilité que la méthode ancienne du fichier discharge.ml ne
permettait pas)
Au passage, ajout d'un modificateur Global aux déclarations
d'implicites et d'arguments scopes pour indiquer qu'elles doivent
perdurer à la sortie de la section
Au passage, suppression de l'objet DISCHARGED-HYPS-MAP et intégration
aux objets VARIABLE/CONSTANT/INDUCTIVE (seule la table des hyps
discharged reste)
Au passage, nettoyage impargs.ml, suppression code mort résiduel du
traducteur etc...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9474 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
Correction d'un bug dans add_glob (list_chop), avec ajout des list_drop_prefix dans lib/util.ml et de drop_dirpath_prefix dans library/libnames.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8768 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8745 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
reference
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7052 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
and ConstrMap to Names
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6747 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
1. when applying a functor F(X) := B to a module M, the obtained module
is no longer B{X.t := M.t for all t}, but B{X.t := b where b is the
body of t in M}. In principle it is now easy to fine tune the behaviour
to choose whether b or M.t must be used. This change implies modifications
both inside and outside the kernel.
2. for each object in the library it is now necessary to define the behaviour
w.r.t. the substitution {X.t := b}. Notice that in many many cases the
pre-existing behaviour w.r.t. the substitution {X.t := M.t} was broken
(in the sense that it used to break several invariants). This commit
fixes the behaviours for most of the objects, excluded
a) coercions: a future commit should allow any term to be declared
as a coercion; moreover the invariant that just a coercion path
exists between two classes will be broken by the instantiation.
b) global references when used as arguments of a few tactics/commands
In all the other cases the behaviour implemented is the one that looks
to me as the one expected by the user (if possible):
[ terminology: not expanded (X.t := M.t) vs expanded (X.t := b) ]
a) argument scopes: not expanded
b) SYNTAXCONSTANT: expanded
c) implicit arguments: not expanded
d) coercions: expansion to be done (for now not expanded)
e) concrete syntax tree for patterns: expanded
f) concrete syntax tree for raw terms: expanded
g) evaluable references (used by unfold, delta expansion, etc.): not
expanded
h) auto's hints: expanded when possible (i.e. when the expansion of the
head of the pattern is rigid)
i) realizers (for program extraction): nothing is done since the actual
code does not look for the realizer of definitions with a body;
however this solution is fragile.
l) syntax and notation: expanded
m) structures and canonical structures: an invariant says that no
parameter can happear in them ==> the substitution always yelds the
original term
n) stuff related to V7 syntax: since this part of the code is doomed
to disappear, I have made no effort to fix a reasonable semantics;
not expanded is the default one applied
o) RefArgTypes: to be understood. For now a warning is issued whether
expanded != not expanded, and the not expanded solution is chosen.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6555 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
the new module kernel/mod_subst.ml.
MOTIVATION: mod_subst is compiled after kernel/term.ml; thus it is now
possible to define substitutions that also delta-expand constants
(by associating the delta-expanded form to the constant name).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6304 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
MOVITATION: in a forthcoming commit the application of a substitution to a
constant will return a constr and not a constant. The application of a
substitution to a kernel_name will return a kernel_name. Thus "constant"
should be use as a kernel name for references that can be delta-expanded.
KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code
that implements "Canonical Structure"s). The ADT is violated once in this
ocaml module. My feeling is that the implementation of "Canonical Structure"s
should be rewritten to avoid this situation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6288 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
interp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4365 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
foncteurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4116 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
list_skipn n l
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3931 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3823 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3379 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3335 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3266 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
|
| |
|
|
|
|
|
|
|
|
|
| |
- Simplification de strength qui est maintenant un simple drapeau Local/Global.
- Export des catégories de déclarations (Lemma/Theorem/Definition/.../
Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml).
- Export des variables de section initialement associées à une déclaration
(nouveau fichier library/dischargedhypsmap.ml).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
|
soubiran
herbelin
msozeau
lmamane
notin
sacerdot
letouzey
coq