aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Collapse)Author
2001-10-22chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les ↵letouzey
options git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2133 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-12Déplacement de global_reference dans Names pour pouvoir lier Nametab à ↵herbelin
grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2112 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-12reparationfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2110 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-10-01correction de deux petits bugs: case_identité trop fort et Anomaly dans le ↵letouzey
toplevel git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2091 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-21Correction due au changement de semantique de Matchdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2049 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-20correction du eta_expanseletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2028 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Report des modifs de Claudioherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2024 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20bug affichage des termes ml fournisletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2022 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20utilisation du nouveau get_sort_family_ofletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2021 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20changements mineurs du testletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2020 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Romegamohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2014 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19ajout du fichier CHANGESletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2004 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19adaptation a la nouvelle syntaxe Extract Inlined Constantletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2001 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Changements de Extraction truc et Recursive Extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2000 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Deux nouvelles optimisations pour Casesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1994 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19MAJ V7.1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1993 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Verification supplementaire avant optimisation singletonletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1991 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19reparation Znemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1989 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-18travail sur le Extract Constantletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1986 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-18Modification de l'emplacement des fichiers pour les setoides.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1982 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-18Romega/names/Makefilemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1980 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-14MAJ vis à vis de la nouvelle non-localité des Remark/Factherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1971 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-12*** empty log message ***mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1955 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-10changement du make depend en vu du make realsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1948 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-10bug de rename_global modulaire corrige'letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1947 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Nettoyage reduce_to_ind et one_step_reduceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1942 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-10Prsingherbelin
- 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@1891 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-07Passage au nouveau Destructherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1882 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1880 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-21Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ↵herbelin
par le nombre d'args inutiles + vérification dans le noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1860 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-18Ajout de la contrib sur les graphesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1857 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-10Setoid_rewrite -> Rewriteclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1847 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-10Ajout des fichiers pour le Ring pour setoidesclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1844 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-10Changement de place de la tactique Setoid_rewriteclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1840 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-10Ajout d'un Ring pour setoidesclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1839 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-05correction bug Omegafilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1826 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@1821 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-02Nettoyage/restructuration des ensembles d'indicateurs de réductionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1819 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-27Reduction du terme preuve fourni par Fielddelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1813 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-06-27Reduction tres significative du terme preuvedelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1811 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-26Les tacticques Setoid_replace/rewrite peuvent maintenant reecrire sous uneclrenard
implication. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1810 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-25Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la ↵herbelin
compilation native powerpc), le nouveau morceau étant g_ltac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1805 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-25liste des equiv exporteeclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1802 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-222 bugs: typevarlist pour inductifs + args pour flexiblesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1800 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-20Ajout d'un Setoid_rewrite et meilleure resolution des petits sous-buts ↵clrenard
générés. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1799 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 05:26:49 +0000