aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-12MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2111 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-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-10-11Bug collision entre les implicites d'un global et les variables locales de ↵herbelin
même nom court git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2108 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-10Incompatibilité entre la prise en compte des univers au niveau des ↵herbelin
tactiques et le test de conversion qui oublie la cumulativité git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2107 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-05Petit oubli à propos de ThinBodyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2105 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-10-05un echo de débogage superfluherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2103 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-05Test de dépendances de ClearBodyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2102 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-03Bug de synthèse du prédicat en présence d'arguments non filtrable; ↵herbelin
correction pour prendre en compte les définitions locales dans le type des inductifs filtrés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2101 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-03Bug d'affichage du prédicat, bug d'affichage des clauses en présence de ↵herbelin
définitions locales dans le type de l'inductif filtré git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2100 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-03Bugs de vérification de la bonne fondation en présence de définitions ↵herbelin
locales dans le type de l'inductif décroissant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2099 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-03coqtop includes itself the needed pathsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2098 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-03MAJ docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2097 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-03Correction messages d'erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2096 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-03Ces fichiers repassent (y restait un bug dans l'inférence du prédicat)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2095 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-03Tests de Cases avec définitions localesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2094 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-02Ajout de dynamiques pour les quotations constr et tacticdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2093 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-02Encapsulage des '<' et '>' pour éviter le regroupement '«'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2092 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-10-01Incompatibilite camlp4 -pp et windows resolu a partir de camlp4 3.01.6herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2090 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-01Il faut camlp4 > 3.01.6 pour windowsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2089 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-01Tests noms longs de modulesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2088 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-30Doc de Ltac, Field et AutoRewrite -> FAITdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2087 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-09-27Ultime Ultimeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2084 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-27Ajout INSTALL.winherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2083 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-27Simplification de deux preuves. En outre ca simplifie leur extraction.letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2082 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-27and_rec redondantletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2081 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-26MAJ V7.1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2080 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-26tools pas fait automatiquementherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2078 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-26Compatibilite Windoz/cygwinherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2077 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-26Compatibilite Windowsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2076 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-26MAJ contribherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2075 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-26Hack pour ajuster les chemins a la mode cygwinherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2074 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-26Compatibilite Windozherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2073 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-26Protection contre erreurs Unixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2072 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-26Le fichier .vo etait ecrit dans un mauvais repertoire si ce dernier etait ↵herbelin
trouve dans le path git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2071 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-25ajout d'un fichier test pour setoidesclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2069 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-25Nouvel emplacement pour coq.specherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2066 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-25correctiontypo SETOIDSVOwerner
BW git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2065 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-25MAJ V7.1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2064 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-25Mise en pageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2063 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 21:49:12 +0000