aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2002-10-02majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3062 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-01Adding the congruence closure tactics (CC and CCsolve).corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3061 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-01Oops...coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3060 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-01backslahs foireuxfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3059 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-01majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3058 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-01Table fonctionnelle dans autorewritecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3057 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-01Vraie substitutivite de autohintscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3055 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-01Cool dev/Makefile'scoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3054 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-01bug de noms long pour eqT.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3053 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-30Comparaisons des types pendant le sous-typage reactivecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3052 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-30majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3050 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-29Activation du hash-consingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3049 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-29Hash-consing pour kernel_nameherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3048 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-29Réparation hash_consingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3047 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-29Complétion filtrageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3046 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-29Que des niveaux d'univers frais dans le type des constantes globalesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3045 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-29Modifs diversesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3044 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-29Que des niveaux d'univers frais dans le type des constantes globalesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3043 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-27Filtrage redondantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3042 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-27passage a ocaml 3.06herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3041 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-27Encore quelques rangements dans Nametab + petits trucscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3039 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3038 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-26suppression de l'axiome eqDomdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3037 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-25preuve d'un axiome restant via Rtopologydesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3036 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-25MAJ pour Rtopologydesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3035 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-25Proprietes topologiques dans Rdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3034 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-25*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3033 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-25Affaiblissement de l'ordre sur Z on demande x < y et seulementmohring
que y (et pas x) soit plus garnd que c git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3032 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-24Un peu (plus) d'ordre dans Nametab...coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3031 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-24Nametab data structure reorganisationcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3030 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-24suite chgt liés aux modulesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3029 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-21Changement de sémantique de Remark : maintenant un global comme les autresherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3028 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-21majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3027 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-20La notation with dependante + affichage dependante de moduels corrigecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3025 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3022 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3021 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3020 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-19portage Correctness (substitutivité pour les modules)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3019 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-18retablissement de Correctness (pas encore teste' cependant)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3016 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-17echappements incorrects dans chainefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3015 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-16Réintroduction de l'expansion des variables de shell et de '~' dans lesherbelin
chemins de fichiers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3012 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-16Un peu plus de flexibilité pour la position du '.' finalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3010 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-16Subst (tout court)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3007 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-13Ajout contribs manquantesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3005 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-11tactique Subst x1 ... xnfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2998 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-09Code mort de AutoRewriteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2993 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-03Amélioration messages d'erreur non inférence implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2987 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-03pretyping/pretyping.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2986 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-21Correctioncoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2976 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-19La notation 'with'. L'interpretation - version preliminairecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2975 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 04:34:02 +0000