aboutsummaryrefslogtreecommitdiff
path: root/pretyping/cases.ml
AgeCommit message (Collapse)Author
2002-06-13Nouvelle version de l'algorithme de compilation du filtrage compatible avec ↵herbelin
une forme expansée des Cases git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2783 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-03Simplification du filtrage si la premiere ligne de motifs est inevitable + ↵herbelin
autres bugs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2665 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-11Deuxième passe sur la localisation des messages d'erreurs sur les evars non ↵herbelin
définies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2633 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-10Amélioration des messages d'erreurs concernant l'inférence des implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2630 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14- Reforme de la gestion des args recursifs (via arbres reguliers)barras
- coqtop -byte -opt bouclait! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2475 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-07petit nettoyage de kernel/inductivebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2460 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-24Réparation bug 'known_dependent'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2426 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-16Correction d'un problème avec les motifs anonymes dépendant dans des ↵herbelin
arguments implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2399 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-15Correction de de Bruijn incorrect pour le cas de dépendances vers l'avantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2396 85f007b7-540e-0410-9357-904b9bb8a0f7
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-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-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-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-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-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-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-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-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-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-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-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-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-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-06-25Bug dépendances non pertinentes (dû à des K-rédex) dans le type des ↵herbelin
branches des Cases non contournées (bug Solange Coupet) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1801 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-16code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1788 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-12Ajout d'une normalisation (beta_iota) pour les predicats de Cases inferes ↵clrenard
automatiquement. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1784 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
ajout automatique des chemins vers les sources au moment du Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-15Correction bug predicat du Cases (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1752 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-12Bug propagation du predicat des Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1749 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-25Bug perte d'alias avec type dependentsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1708 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-15Bug affichage ordre des variables d'un patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1592 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-13Mise en place d'un test de clauses non utiliseesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1589 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-28amelioration de la structure des universbarras
elimination des compteurs globaux de metas et d'evars du noyau nettoyage de safe_typing.ml (plus de flags) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1497 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-14Alias suite + bugs divers et variésherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1466 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-12Rien au lieu erreur si plusieurs cas par défaut; quasi-achèvement alias ↵herbelin
dépendants git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1452 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-11Avancée vers la prise compte des alias dépendants; prise en compte des ↵herbelin
clauses par défaut dans l'ordre; amélioration messages d'erreurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1446 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-05Pb génération noms Cases + mise en place mécanisme d'histoire du filtrage ↵herbelin
pour les alias git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1422 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14uniformisation avec constr des lieurs dans rawterm/patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1377 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-07Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1340 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Bug prédicatherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1199 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-18Amélioration message d'erreur mauvais prédicatherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1142 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-16Suppression du warning several default clausesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1134 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 05:59:52 +0000