aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2001-12-19Insertion unification non seulement en tête mais à l'intérieur des motifs ↵herbelin
(permet p.ex. de traiter le motif (Some O)) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2322 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18Grossière erreur de typageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2305 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18Nettoyage exceptions liées au vieux Caseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2304 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-18Nettoyage exceptions liées au vieux Case; réparation du try with UserError ↵herbelin
mal nommé dans findtype git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2303 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13Contournement du problème des evars de type, typées par défaut dans Type ↵herbelin
(suite) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2295 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13Contournement du problème des evars de type, typées par défaut dans Typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2293 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13compat ocaml 3.03filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-11Mise en place de coercion dans les motifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2285 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-29nouvel algo de conversion plus uniformebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-22La mise en forme normale du prédicat d'élimination était un peu trop ↵herbelin
violente pour la compatibilité de la synthèse des evars git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2241 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Quelques autres petits problèmes résolus...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2239 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 16:45:48 +0000