aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* correction du eta_expanseGravatar letouzey2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2028 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ V7.1Gravatar herbelin2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2027 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nombre magique pour la V7.1Gravatar herbelin2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2026 85f007b7-540e-0410-9357-904b9bb8a0f7
* Le prédicat du vieux Case ne doit pas contenir d'univers algébrique même ↵Gravatar herbelin2001-09-20
| | | | | | 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
* Report des modifs de ClaudioGravatar herbelin2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2024 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pas de warning pour le -I . par défaut de CoqGravatar herbelin2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2023 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug affichage des termes ml fournisGravatar letouzey2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2022 85f007b7-540e-0410-9357-904b9bb8a0f7
* utilisation du nouveau get_sort_family_ofGravatar letouzey2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2021 85f007b7-540e-0410-9357-904b9bb8a0f7
* changements mineurs du testGravatar letouzey2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2020 85f007b7-540e-0410-9357-904b9bb8a0f7
* warning silencieuxGravatar filliatr2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2019 85f007b7-540e-0410-9357-904b9bb8a0f7
* version V7.1Gravatar herbelin2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2018 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restriction de l'avertissement add_loadpath au mode verbeuxGravatar herbelin2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2017 85f007b7-540e-0410-9357-904b9bb8a0f7
* On ignore les répertoires qui ne correspondent pas à des identsGravatar herbelin2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2016 85f007b7-540e-0410-9357-904b9bb8a0f7
* On ignore les répertoires invisibles dans all_subdirsGravatar herbelin2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2015 85f007b7-540e-0410-9357-904b9bb8a0f7
* RomegaGravatar mohring2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2014 85f007b7-540e-0410-9357-904b9bb8a0f7
* let-in dans RefineGravatar filliatr2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2013 85f007b7-540e-0410-9357-904b9bb8a0f7
* Refine et let-inGravatar filliatr2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2012 85f007b7-540e-0410-9357-904b9bb8a0f7
* Blindage, de peur que des types entrant non en forme normale ne provoque des ↵Gravatar herbelin2001-09-19
| | | | | | 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
* Nouvelle fonction get_sort_family_of pour calculer la famille dans lequel ↵Gravatar herbelin2001-09-19
| | | | | | vit un type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2010 85f007b7-540e-0410-9357-904b9bb8a0f7
* Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles ↵Gravatar herbelin2001-09-19
| | | | | | des sortes (InProp, InSet, InType) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2009 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle fonction sort_family_of pour calculer la famille dans lequel vit un ↵Gravatar herbelin2001-09-19
| | | | | | type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2008 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intégration partielle des modifs de la V7.0Gravatar herbelin2001-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2007 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affichage des dir_path videGravatar herbelin2001-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2006 85f007b7-540e-0410-9357-904b9bb8a0f7
* Autorisation de surcharge d'un -R par un -IGravatar herbelin2001-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2005 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout du fichier CHANGESGravatar letouzey2001-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2004 85f007b7-540e-0410-9357-904b9bb8a0f7
* la cible all était incomplèteGravatar filliatr2001-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2003 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection hd d'une liste videGravatar herbelin2001-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2002 85f007b7-540e-0410-9357-904b9bb8a0f7
* adaptation a la nouvelle syntaxe Extract Inlined ConstantGravatar letouzey2001-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2001 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changements de Extraction truc et Recursive ExtractionGravatar letouzey2001-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2000 85f007b7-540e-0410-9357-904b9bb8a0f7
* make install dans coq_makefile et repertoire associe user-contrib ajoute au ↵Gravatar filliatr2001-09-19
| | | | | | load path au demarrage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1999 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et ↵Gravatar herbelin2001-09-19
| | | | | | le «load» des Remark/Fact git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1998 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques signes extérieurs de la sémantique de Remark, question visibilitéGravatar herbelin2001-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1997 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ces fichiers décrivent des comportements peut-être souhaités mais ↵Gravatar herbelin2001-09-19
| | | | | | actuellement non implantés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1996 85f007b7-540e-0410-9357-904b9bb8a0f7
* Comportements peut-être souhaités mais en tout cas non officiellement pris ↵Gravatar herbelin2001-09-19
| | | | | | en compte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1995 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deux nouvelles optimisations pour CasesGravatar letouzey2001-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1994 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ V7.1Gravatar herbelin2001-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1993 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement des setoides.Gravatar clrenard2001-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1992 85f007b7-540e-0410-9357-904b9bb8a0f7
* Verification supplementaire avant optimisation singletonGravatar letouzey2001-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1991 85f007b7-540e-0410-9357-904b9bb8a0f7
* TypoGravatar herbelin2001-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1990 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation ZneGravatar mohring2001-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1989 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative de canonisation des répertoires physiquesGravatar herbelin2001-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1988 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place de noms contenant la section pour Fact et RemarkGravatar herbelin2001-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1987 85f007b7-540e-0410-9357-904b9bb8a0f7
* travail sur le Extract ConstantGravatar letouzey2001-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1986 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques heuristiques pour gérer des représentations similaires de paths ↵Gravatar herbelin2001-09-18
| | | | | | syntaxiquement différents git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1985 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une option et d'une fonction compile pour fabriquer les .voGravatar herbelin2001-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1984 85f007b7-540e-0410-9357-904b9bb8a0f7
* update sur les tactiquesGravatar mayero2001-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1983 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de l'emplacement des fichiers pour les setoides.Gravatar clrenard2001-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1982 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression du message d'erreur si une coercion mettant en jeu des locaux ↵Gravatar herbelin2001-09-18
| | | | | | 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
* Romega/names/MakefileGravatar mohring2001-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1980 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug discharge d'une déclaration de coercion pour une constante non définie ↵Gravatar herbelin2001-09-18
| | | | | | dans la section courante git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1979 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 01:54:01 +0000