aboutsummaryrefslogtreecommitdiff
path: root/library/library.ml
AgeCommit message (Collapse)Author
2005-02-05Localisation des libraries compilées uniquement via la structure du ↵herbelin
loadpath (sinon des modules de même nom chargés via un Export sont trouvés avant ceux officiellement dans le chemin) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6689 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17Bug 'Locate Library lib' quand 'lib' est aussi un moduleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6318 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-14MAJ numéro magiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5674 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30The XML exportation hook for require is now active for:sacerdot
- Require id. - Require Export id. - Require "file". - Require Export "file". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5618 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-29Crocret xml pour Requireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5598 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15preparation packages V8.0-cdrombarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5489 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-28Bug de Require multipleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5261 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-23Changement numero magique; message d'erreur en cas de mauvaise syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5130 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Mise en place d'un mecanisme ne chargeant pas les preuves opaquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4539 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19but Require dans une Sectionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4028 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-15table des modules charges (Library.compunit_cache) synchronizee (pour CoqIde ↵filliatr
notamment) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4025 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-03release 7.4; changement magic numberfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3652 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-09Export M + Module M <: SIGcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3494 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-19Petit netoyage dans libcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3463 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-29Préservation de la cohérence du cache en cas d'erreur au chargementherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3189 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-12Forcer la réouverture d'un fichier explicitement requis même si leherbelin
fichier a déjà été ouvert précédemment (peut-être indirectement) par un autre Require. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3115 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-03Protection des tactiques contre l'utilisation sans le bon contexte de thoriesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2746 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-15MAJ V7.3herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2689 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-24Correction de l'ordre des open (sachant que de toutes façons, unherbelin
Require au milieu d'un module sera considéré comme situé au début du module chargé) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2432 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-18Pas d'assert false dans un try with !herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2414 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-18Plusieurs arguments autorisés pour Require et Read Module; mise en place ↵herbelin
d'un mécanisme pour se souvenir de l'ordre des Open (mais pas activé); suppression du champ string dans le summary REQUIRE git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2411 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-07Suppression de la dépendance des .vo en le nom physique des modulesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2379 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19MAJ nombre magiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2335 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-17probleme des Require dans les sectionsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2301 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13compat ocaml 3.03filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-05Rustine pour garder la compatibilité avec la 7.1 pour l'ordre des imports ↵herbelin
sans toutefois adopter l'ordre textuel git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2266 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05GROS COMMIT:barras
- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-17Abstraction de l'immplementation de dirpath et implementation dans l'autre ↵herbelin
sens pour plus de partage entre chemins git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2126 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-24One more boolean test bugherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2057 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-24Bug test booléenherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2056 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Nombre magique pour la V7.1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2026 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Pas de warning pour le -I . par défaut de Coqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2023 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20warning silencieuxfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2019 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Restriction de l'avertissement add_loadpath au mode verbeuxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2017 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Autorisation de surcharge d'un -R par un -Iherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2005 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1990 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-18Tentative de canonisation des répertoires physiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1988 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-18Quelques heuristiques pour gérer des représentations similaires de paths ↵herbelin
syntaxiquement différents git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1985 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-07Suppression des library roots, on teste si un nom est absolu autrementherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1927 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-10Parsingherbelin
- Typage renforcé dans les grammaires (distinction des vars et des metavars) - Disparition de SLAM au profit de ABSTRACT - Paths primitifs dans les quotations (syntaxe concrète à base de .) - Mise en place de identifier dès le type ast - Protection de identifier contre les effets de bord via un String.copy - Utilisation de module_ident (= identifier) dans les dir_path (au lieu de string) Table des noms qualifiés - Remplacement de la table de visibilité par une table qui ne cache plus les noms de modules et sections mais seulement les noms des constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel module A déjà existant : seuls les noms de constructions de l'ancien A qui existent aussi dans le nouveau A seront cachés) - Renoncement à la possibilité d'accéder les formes non déchargées des constantes définies à l'intérieur de sections et simplification connexes (suppression de END-SECTION, une seule table de noms qui ne survit pas au discharge) - Utilisation de noms longs pour les modules, de noms qualifiés pour Require and co, tests de cohérence; pour être cohérent avec la non survie des tables de noms à la sortie des section, les require à l'intérieur d'une section eux aussi sont refaits à la fermeture de la section git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1889 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-09Backtrack sur le warning Require en Section: trop contraignantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1834 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-05Avertissement contre les Require dans le corps d'une sectionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1829 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-07quelques bug reports mineursbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1733 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-09protection contre certaines exceptions levees par marshal_{in,out}barras
possibilite de declarer une def syntaxique comme infix (utilise par FTA) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1442 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-06on gele apres un Require => meilleures performances memoire, en particulier ↵filliatr
pour Proof General git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1433 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 22:27:33 +0000