aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-18Quelques heuristiques pour gérer des représentations similaires de paths ↵herbelin
syntaxiquement différents git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1985 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-18Ajout d'une option et d'une fonction compile pour fabriquer les .voherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1984 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-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-18Suppression du message d'erreur si une coercion mettant en jeu des locaux ↵herbelin
n'est pas déclarée locale (le discharge fonctionnera bien silencieusement et c'est compatible V6.3) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1981 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-18Bug discharge d'une déclaration de coercion pour une constante non définie ↵herbelin
dans la section courante git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1979 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-18modif test constmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1977 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-17Blindage de Show Introletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1976 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-17unification avec TOUS les sous-termes ( (plus ?) ne s'unifiait pas avec lesbarras
sous-termes de (plus O O) ). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1975 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-17quotation des noms de fichiers pour eviter une mauvaise interpretation des \barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1974 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-14Search prenait en compte le contenu des sections alors que celui-ci n'existe ↵herbelin
plus git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1972 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-14Correction confusion VarNode/SectionVarNode (d'où bug Hints Unfold nom_local)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1970 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-14Transformation de Remark/Fact en constantes non visibles sans qualificationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1969 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-14Ajout syntaxe "Assert H:T."herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1968 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-14L'instantiation des evars quand un produit ou une sorte étaient attendus ↵herbelin
n'était pas fait git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1967 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-14L'instantiation des evars quand un produit ou une sorte étaient attendus ↵herbelin
n'était pas fait git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1966 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-14exceptionsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1965 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-14mauvais rattrapage d'exceptionbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1964 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-13Only CHANGES !herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1963 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-13Prise en compte qualid dans Hint Unfoldherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1961 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-13Syntaxe des Hintsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1960 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-13uniformité des cibles pour les contribsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1959 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-13mise à jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1958 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-13eclaircissement du codecourant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1957 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-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-12Rustine pour gérer inject_natherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1954 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-11Un look un peu plus avenant aux productions des règles de grammaireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1953 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-11Du bon usage des commentaires coqwebherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1952 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-11Conformité des commentaires au format coqwebherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1951 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-10Hack pour gérer les univers dans les prédicats de Cases synthétisésherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1949 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-10Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ↵herbelin
éliminations, pour éviter les collisions avec les univers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1946 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-10Un conv aurait dû être un conv_leqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1945 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-10Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ↵herbelin
éliminations, pour éviter les collisions avec les univers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1944 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Légère modification lookup_eliminatorherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1943 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-09-09Passage aux univers algébriquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1941 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Passage aux univers algébriquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1940 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Amélioration check_module_nameherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1939 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Préparation à la mise en place d'univers algébriquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1938 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Suppression de Type_1, inutile, et non prévu dans le modèle des univers ↵herbelin
algébriques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1937 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 02:07:02 +0000