aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2001-09-20Le prédicat du vieux Case ne doit pas contenir d'univers algébrique même ↵herbelin
quand il est synthétisé à partir du type des branches git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2025 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-20Pas de warning pour le -I . par défaut de Coqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2023 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-20warning silencieuxfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2019 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20version V7.1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2018 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Restriction de l'avertissement add_loadpath au mode verbeuxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2017 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20On ignore les répertoires qui ne correspondent pas à des identsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2016 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20On ignore les répertoires invisibles dans all_subdirsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2015 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-20let-in dans Refinefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2013 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Refine et let-infilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2012 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Blindage, de peur que des types entrant non en forme normale ne provoque des ↵herbelin
calculs sur les univers dans get_sort_family_of git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2011 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Nouvelle fonction get_sort_family_of pour calculer la famille dans lequel ↵herbelin
vit un type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2010 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles ↵herbelin
des sortes (InProp, InSet, InType) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2009 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Nouvelle fonction sort_family_of pour calculer la famille dans lequel vit un ↵herbelin
type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2008 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Intégration partielle des modifs de la V7.0herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2007 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Affichage des dir_path videherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2006 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Autorisation de surcharge d'un -R par un -Iherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2005 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-19la cible all était incomplètefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2003 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Protection hd d'une liste videherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2002 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-19make install dans coq_makefile et repertoire associe user-contrib ajoute au ↵filliatr
load path au demarrage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1999 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et ↵herbelin
le «load» des Remark/Fact git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1998 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Quelques signes extérieurs de la sémantique de Remark, question visibilitéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1997 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Ces fichiers décrivent des comportements peut-être souhaités mais ↵herbelin
actuellement non implantés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1996 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Comportements peut-être souhaités mais en tout cas non officiellement pris ↵herbelin
en compte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1995 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-19Deplacement des setoides.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1992 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-19Typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1990 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-18Tentative de canonisation des répertoires physiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1988 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-18Mise en place de noms contenant la section pour Fact et Remarkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1987 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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 00:42:01 +0000