aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2001-11-21Simplification de la propagation du prédicat, bugs, et messages d'erreursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2234 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Solution partielle au problème des alias dépendants pour les rendre ↵herbelin
compatibles avec l'utilisation de la contrainte de type comme guide de la synthèse du prédicat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2229 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Prise en compte des coercions pour typer les branches lorsqu'il y a une ↵herbelin
contrainte de type sur le résultat du Cases git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2221 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Ajout make_arity_signatureherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2219 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Correction bug contrainte de valeur trop restrictive sur le typage du type ↵herbelin
du Cast git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2214 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Bug mauvaise instanceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2212 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Fusion de declare/add_constant, declare/add_parameter et add_discharged_constantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2211 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-19Bug nommage des fonctions définies par récursion mutuelleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2205 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-19Re-installation de l'affichage des globaux par des noms courtsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2200 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-19Remise en place du Cast pour Correctnessherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2199 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-17User Casts are for helping pretyping, experimentally not to be keptherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2198 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-09Nettoyage coercions et classesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2179 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-09code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2176 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-08Introduction d'univers frais dans les types implicites engendrés par le ↵herbelin
prétypage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2172 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-08Rétablissement de la persistance des Cast; typage des LetIn sans recours à ↵herbelin
Cast git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2171 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-06corrections mineures suite au commit de restructuration du noyaubarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2165 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2163 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05GROS COMMIT:barras
- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-30Reorganisation de Goption. Passage des options l'utilisant en synchroneletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2145 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-29Amérioration message d'erreur en cas d'échec du filtrage de premier ordreherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2144 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-16Nettoyage Recordobj et conséquencesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2122 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-15Insertion automatique des motifs de let-in s'il ne sont pas explicitement ↵herbelin
mentionnés (pour compatibilité) (2 ème) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2118 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-15Rustine pour rendre les messages d'erreurs de la compilation des Cases plus ↵herbelin
lisibles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2117 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-15Insertion automatique des motifs de let-in s'il ne sont pas explicitement ↵herbelin
mentionnés (pour compatibilité) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2114 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-03Bug de synthèse du prédicat en présence d'arguments non filtrable; ↵herbelin
correction pour prendre en compte les définitions locales dans le type des inductifs filtrés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2101 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-03Bug d'affichage du prédicat, bug d'affichage des clauses en présence de ↵herbelin
définitions locales dans le type de l'inductif filtré git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2100 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-02Ajout de dynamiques pour les quotations constr et tacticdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2093 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-21Réparation des options Set Printing and coherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2052 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Transparentbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
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-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-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-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-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-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@1940 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Préparation du prétypage à la mise en place d'univers algébriquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1936 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-07Extension à Cases et Fix de la réduction pas à pas vers un produit (Red)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1928 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-04erreur de pretty-print lors de l'affichage de termes avec de Bruijn non liesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1920 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-13bug de Bruijnherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1896 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-10Parsingherbelin
- Typage renforcé dans les grammaires (distinction des vars et des metavars) - Disparition de SLAM au profit de ABSTRACT - Paths primitifs dans les quotations (syntaxe concrète à base de .) - Mise en place de identifier dès le type ast - Protection de identifier contre les effets de bord via un String.copy - Utilisation de module_ident (= identifier) dans les dir_path (au lieu de string) Table des noms qualifiés - Remplacement de la table de visibilité par une table qui ne cache plus les noms de modules et sections mais seulement les noms des constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel module A déjà existant : seuls les noms de constructions de l'ancien A qui existent aussi dans le nouveau A seront cachés) - Renoncement à la possibilité d'accéder les formes non déchargées des constantes définies à l'intérieur de sections et simplification connexes (suppression de END-SECTION, une seule table de noms qui ne survit pas au discharge) - Utilisation de noms longs pour les modules, de noms qualifiés pour Require and co, tests de cohérence; pour être cohérent avec la non survie des tables de noms à la sortie des section, les require à l'intérieur d'une section eux aussi sont refaits à la fermeture de la section git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1889 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-24Bug Simplherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1864 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-21Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ↵herbelin
par le nombre d'args inutiles + vérification dans le noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1862 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 23:56:40 +0000