aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2163 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-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-30Ajout du printer de tactiques + modif du Dynamic ocamldelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2086 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-06-27correction d'un bug de Correctness (pour Y Bertot)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1812 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-29Retablissement de minicoqcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1773 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-29Facilites pour le debogguage des univers.coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1772 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
ajout automatique des chemins vers les sources au moment du Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-15Modification pour passage p-automatesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1753 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-10ajout d'un afficher de contexte et d'une fonction constbody_of_stringletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1739 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-03Make sure that the COQTOP variable is really used, when it is set.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1523 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-06modifs pour extraction; bug coqmktopfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1428 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-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1420 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1419 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01nouvelle implantation de la reductionbarras
suppression de IsXtra du noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1416 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-30MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1294 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-18MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1148 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Printermohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1117 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Bug sur commit précédentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1103 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Enfin trouvé la cause d'exception; suppression de la capsule de rattrapageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1102 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-05Ajout du répertoire config utilisé par System en localherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1053 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-04Ajout de constr_of_stringmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1044 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29ajout constr_displayfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1032 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29-I configmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1029 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Prise en compte qualidherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@963 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@954 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24Paramètrage de ocamldebug-v7 par configure à partir d'un 'template'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@949 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-22Reparation bug mutuels indmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@916 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-11Gros hack pour afficher les universherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@846 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-02suppression des (* open Generic *)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@793 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-27g_natsyntax et g_zsyntax maintenant toujours linkesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@773 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-23MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@736 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@729 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@700 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-06MAJ pr_uniherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@666 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-04Commit malencontreux sur précédente versionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@655 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-04Mise en conformité nouveau Simpl pour Fixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@654 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-03MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@641 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Renommage AppL en Appherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@635 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@629 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-26MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@614 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-14MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@606 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-12MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@598 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Ajout d'un LetIn primitif.herbelin
Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@591 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-06Canonisation de certains noms dans Pretyping, Asterm et Safe_typingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@586 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:56:40 +0000