aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2002-08-19MAJ .dependcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2974 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-19Pretty-printing preliminaire des modules, commandescoq
Print Module qid. Print Module Type qid. et affichage pendant Print All. Tout ca est preliminare, seuls les noms des composants sont affiches et non pas les corps... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2973 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-17Suppression automatique du corps des définitions locales opaques dansherbelin
les contextes de preuves git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2972 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-16correction de bugs:barras
- subst_term_gen ne depliait pas les constantes locales de maniere uniforme - la tactique Simpl ne simplifiait pas les constantes definies dans le contexte de but - la conversion d'un constr vers identificateur ne prenait pas en compte les inductifs et constructeurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2971 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-16Encore quelques tests sur modules...coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2970 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-16Strengthenning rules for modules + No modules in sectionscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2969 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-15Test for redundant clausesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2968 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-14Test affichage optimal des coercionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2967 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-14MAJ depend.coqcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2966 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 08:52:51 +0000