aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/lib.ml
Commit message (Collapse)AuthorAge
* Reset Initial uniquement interactivementGravatar herbelin2003-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5113 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de Declare juste à la fin de interp pour pouvoir accéder à ↵Gravatar herbelin2003-09-12
| | | | | | interp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4365 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIde : but reset_modGravatar filliatr2003-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4030 85f007b7-540e-0410-9357-904b9bb8a0f7
* configure et make install s'occupent de CoqIde tout seulsGravatar filliatr2003-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4029 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout d'une fonction reset_modGravatar monate2003-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3791 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour satisfaire ProofGeneralGravatar coq2003-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3634 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petit netoyage dans libGravatar coq2002-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3463 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
| | | | | | | | | | | | | | | - 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
* Strengthenning rules for modules + No modules in sectionsGravatar coq2002-08-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
* compat ocaml 3.03Gravatar filliatr2001-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
* - condition de garde (suite)Gravatar barras2001-12-10
| | | | | | | - commande Back git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2283 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
* corrections mineures suite au commit de restructuration du noyauGravatar barras2001-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2165 85f007b7-540e-0410-9357-904b9bb8a0f7
* GROS COMMIT:Gravatar barras2001-11-05
| | | | | | | | | | - 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
* Abstraction de l'immplementation de dirpath et implementation dans l'autre ↵Gravatar herbelin2001-10-17
| | | | | | 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
* Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et ↵Gravatar herbelin2001-09-19
| | | | | | le «load» des Remark/Fact git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1998 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place de noms contenant la section pour Fact et RemarkGravatar herbelin2001-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1987 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rétablissement de Print SectionGravatar herbelin2001-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1926 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug default module name (2eme)Gravatar herbelin2001-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1924 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug default module nameGravatar herbelin2001-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1923 85f007b7-540e-0410-9357-904b9bb8a0f7
* ParsingGravatar herbelin2001-08-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - 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
* Avertissement contre les Require dans le corps d'une sectionGravatar herbelin2001-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1829 85f007b7-540e-0410-9357-904b9bb8a0f7
* entetesGravatar filliatr2001-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug Reset et SectionsGravatar filliatr2001-02-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1410 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test pour empêcher 2 sections de même nomsGravatar herbelin2000-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1172 85f007b7-540e-0410-9357-904b9bb8a0f7
* PédagogieGravatar herbelin2000-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1152 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug des locaux au premier niveau des modules qui disparaissaient de ↵Gravatar herbelin2000-12-15
| | | | | | l'environnement (changement de is_section_p) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1120 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reparation conditions de positivites inductifs, echange dans add_entryGravatar mohring2000-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1057 85f007b7-540e-0410-9357-904b9bb8a0f7
* La zone par défaut pour le nommage des modules est ScratchGravatar herbelin2000-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1018 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte du repertoire dans le section path; utilisation de dirpath ↵Gravatar herbelin2000-11-28
| | | | | | pour les noms de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1005 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametabGravatar filliatr2000-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@947 85f007b7-540e-0410-9357-904b9bb8a0f7
* certains effets disparaissent a la sortie des sections, d'autres non (selon ↵Gravatar filliatr2000-11-24
| | | | | | Summary.survive_section) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@945 85f007b7-540e-0410-9357-904b9bb8a0f7
* reset_name: try / with juste autour de find_entry_p (=> propage lesGravatar filliatr2000-11-21
| | | | | | | vraies erreurs de reset_to s'il y en a) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@908 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout d'un frozen_state après la fermeture d'une section (sinon bug !)Gravatar filliatr2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@906 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction bug ResetGravatar filliatr2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@898 85f007b7-540e-0410-9357-904b9bb8a0f7
* separation calcul des implicites et declaration des constantes / inductifs / ↵Gravatar filliatr2000-11-21
| | | | | | variables git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@897 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petit bug entre close_section'sGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@894 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une Nametab et d'un flag export aux ClosedSection; on applique ↵Gravatar herbelin2000-11-20
| | | | | | export_objet aussi aux sections git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@861 85f007b7-540e-0410-9357-904b9bb8a0f7
* methode exportGravatar filliatr2000-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@851 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ↵Gravatar herbelin2000-11-06
| | | | | | DischargeAt) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@811 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug pop_path_prefix : List.rev manquantGravatar herbelin2000-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@760 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction bug univers (dummy_univ)Gravatar filliatr2000-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@664 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> ↵Gravatar filliatr2000-06-21
| | | | | | .vo plus petits git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@514 85f007b7-540e-0410-9357-904b9bb8a0f7
* gros commit de tout ce que j'ai fait pendant les vacances :Gravatar filliatr2000-01-21
| | | | | | | | | | - tactics/Equality - debug du discharge - constr_of_compattern implante vite fait / mal fait en attendant mieux - theories/Logic (ne passe pas entierrement) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@280 85f007b7-540e-0410-9357-904b9bb8a0f7
* sauvegarde de la valeur de module_nameGravatar filliatr1999-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@253 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jour de refiner.ml (reports de modifs de la V6.3)Gravatar barras1999-12-13
| | | | | | | bug possible dans lib.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@250 85f007b7-540e-0410-9357-904b9bb8a0f7
* modulesGravatar filliatr1999-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@238 85f007b7-540e-0410-9357-904b9bb8a0f7
* debug resetGravatar filliatr1999-12-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@229 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 10:15:01 +0000