aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Collapse)Author
2002-05-15MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2690 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-15mention -dump-globfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2687 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2686 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14Ajout de la modification des sortes d'eliminationmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2681 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-13Pas de projection si le nom d'un champ est '_' dans un Recordherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2675 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-06MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2666 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-12Intuitioncourant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2641 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-12*** empty log message ***courant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2639 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-10MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2625 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-15changements récents dans l'extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2536 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-18modifs ZArith & Chineseletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2407 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-15MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2398 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-21Extension de Evenherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2368 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-21maj CHANGES extraction + bug extraction & _letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2359 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-20MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2358 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2349 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19Changements Realsdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2342 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2327 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2307 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2298 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-12MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2290 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-06Majherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2278 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-22MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2242 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2237 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21documentation de mes actions recentes sur les theories (PL)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2233 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-16MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2197 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-16MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2123 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-12MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2111 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-05Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs ↵herbelin
'ClearBody H' et 'Assert H := c' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2104 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-26Ultime MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2079 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-25*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2070 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-25Qqes oublisherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2068 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-25Ajout d'un résumé des modificationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2067 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-25Mise en pageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2062 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-24MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2053 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-21Vers la fin de la restructurationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2048 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Intégration partielle des modifs de la V7.0herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2007 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-18update sur les tactiquesmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1983 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-18Modif pour Ltac et ajout de Fielddelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1978 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-14MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1973 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-13Structuration et traductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1962 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-13explications modifications Tautocourant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1956 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-11MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1950 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1932 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-07MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1929 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-07Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ↵herbelin
tactique primitive Cut basé sur un Let non dépendant; amélioration efficacité ancien Cut git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1883 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-09MAJ de la MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1836 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-09MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1835 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-02Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans ↵herbelin
Compute, nouveaux flags utilisateurs pour Evar et Zeta git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1820 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 11:02:36 +0000