| Age | Commit message (Collapse) | Author |
|---|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
only used to allow a module to be ended before the summaries were
restored what can be solved by moving upwards the place where the
summaries are restored).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12275 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
|
|
constante par defaut pour les nouveaux types plutot qu'echouer;
avertissement plutot qu'echec en cas de foncteur; nommage systematique
des LetIn -- p.ex. functional induction engendre des LetIn non nommes --;
branchement de la fonction de normalisation de tete evitant CProp
sur Closure au lieu de Tacred afin de garantir la f.n. de tete)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9902 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
|
|
delay some computation from before to after caching time + various simplifications and uniformisations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6748 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@4534 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
|
