aboutsummaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
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-27Changement Filename.is_relative en Filename.is_implicit, plus pertinentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2710 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-10Amélioration des messages d'erreurs concernant l'inférence des implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2630 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-28ajout option_compareherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2499 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14- Reforme de la gestion des args recursifs (via arbres reguliers)barras
- coqtop -byte -opt bouclait! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2475 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14option -dump-glob pour coqdocfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-30ajout list_split3, pr_semicolon et pr_barherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2444 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-18List.map avec ordre des effets de bord garantiherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2410 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-18Le chargement des coercions est nécessaire même si le module n'est pas ouvertherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2409 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-18code redondant avec is_verboseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2408 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-10Ajout flushherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2389 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19reparation du make depend et du .dependletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2334 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-11-29nouvel algo de conversion plus uniformebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-17Nouvelle fonctionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2125 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Transparentbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20On ignore les répertoires invisibles dans all_subdirsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2015 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-10Bugherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1892 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-10Prise en compte des strings et des flottants dans les statistiques de ↵herbelin
tailles mémoire git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1890 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-08-05Nouveau profiler compatible avec ocaml >= 3.01herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1871 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-01MAJ vis à vis de ocaml 3.01herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1866 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-28option -qualityfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1767 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-09nettoyage extractionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1737 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-05-03Changement de la structure des points fixesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19*** empty log message ***courant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1612 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-05array_fold_left_ifilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1550 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-03utilisation de Options.if_verbosefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1519 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-23amelioration de la consommation memoire de la conversion en eta-expansantbarras
les definitions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1483 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-13passage ocaml 3.01filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1460 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-12Ajout list_map3herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1453 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-06EAutod (debug)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1429 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-05module Explore générique et réécriture EAuto avec ce module; occur check ↵filliatr
dans clenv_merge git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1425 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-26export open_trapping_failure pour contrib/extractionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1401 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14Mise en place d'un système optionnel de discharge immédiat; prise en ↵herbelin
compte des défs locales dans les arguments des inductifs; nettoyage divers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1388 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14Restructurationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1378 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-09option -m (utilisation memoire)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1366 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-08simplification du make depend; fonctions de stat. util. memoire dans ↵filliatr
certains modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1355 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-05calcul des dependances camlp4 et production directe ml4 -> cmo (avec Judicael)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1325 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-02Retire le warning statmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1313 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-31Ajout d'espace dans les règles d'affichage des infix si des lettres ↵herbelin
figurent dans le token git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1297 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-24Ajout flush, diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1276 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-24Protection contre l'échec de Unix.statherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1274 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-19Bugs encoreherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1256 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-15Raffinementsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1251 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-14Petit bug encoreherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1250 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 09:27:08 +0000