aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.ml
Commit message (Expand)AuthorAge
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...Gravatar letouzey2003-04-16
* Correction bug #261 + amélioration nommageGravatar herbelin2003-04-01
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Vraie substitutivite de autohintsGravatar coq2002-10-01
* pretyping/pretyping.mlGravatar herbelin2002-09-03
* Renoncement à distinguer les types "constr" et "types"; nettoyageGravatar herbelin2002-08-13
* Nouvelle version de l'algorithme de compilation du filtrage compatible avec u...Gravatar herbelin2002-06-13
* Simplification du filtrage si la premiere ligne de motifs est inevitable + au...Gravatar herbelin2002-05-03
* Deuxième passe sur la localisation des messages d'erreurs sur les evars non ...Gravatar herbelin2002-04-11
* Amélioration des messages d'erreurs concernant l'inférence des implicitesGravatar herbelin2002-04-10
* - Reforme de la gestion des args recursifs (via arbres reguliers)Gravatar barras2002-02-14
* petit nettoyage de kernel/inductiveGravatar barras2002-02-07
* Réparation bug 'known_dependent'Gravatar herbelin2002-01-24
* Correction d'un problème avec les motifs anonymes dépendant dans des argume...Gravatar herbelin2002-01-16
* Correction de de Bruijn incorrect pour le cas de dépendances vers l'avantGravatar herbelin2002-01-15
* Insertion unification non seulement en tête mais à l'intérieur des motifs ...Gravatar herbelin2001-12-19
* Nettoyage exceptions liées au vieux CaseGravatar herbelin2001-12-18
* compat ocaml 3.03Gravatar filliatr2001-12-13
* Mise en place de coercion dans les motifsGravatar herbelin2001-12-11
* La mise en forme normale du prédicat d'élimination était un peu trop viole...Gravatar herbelin2001-11-22
* Quelques autres petits problèmes résolus...Gravatar herbelin2001-11-21
* Simplification de la propagation du prédicat, bugs, et messages d'erreursGravatar herbelin2001-11-21
* Solution partielle au problème des alias dépendants pour les rendre compati...Gravatar herbelin2001-11-21
* Prise en compte des coercions pour typer les branches lorsqu'il y a une contr...Gravatar herbelin2001-11-21
* Introduction d'univers frais dans les types implicites engendrés par le pré...Gravatar herbelin2001-11-08
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* GROS COMMIT:Gravatar barras2001-11-05
* Insertion automatique des motifs de let-in s'il ne sont pas explicitement men...Gravatar herbelin2001-10-15
* Insertion automatique des motifs de let-in s'il ne sont pas explicitement men...Gravatar herbelin2001-10-15
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* Bug de synthèse du prédicat en présence d'arguments non filtrable; correct...Gravatar herbelin2001-10-03
* Ajout de dynamiques pour les quotations constr et tacticGravatar delahaye2001-10-02
* Le prédicat du vieux Case ne doit pas contenir d'univers algébrique même q...Gravatar herbelin2001-09-20
* Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...Gravatar herbelin2001-09-19
* Hack pour gérer les univers dans les prédicats de Cases synthétisésGravatar herbelin2001-09-10
* Préparation du prétypage à la mise en place d'univers algébriquesGravatar herbelin2001-09-09
* Bug dépendances non pertinentes (dû à des K-rédex) dans le type des branc...Gravatar herbelin2001-06-25
* code mortGravatar herbelin2001-06-16
* Ajout d'une normalisation (beta_iota) pour les predicats de Cases inferes aut...Gravatar clrenard2001-06-12
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
* Correction bug predicat du Cases (suite)Gravatar herbelin2001-05-15
* Bug propagation du predicat des CasesGravatar herbelin2001-05-12
* Bug perte d'alias avec type dependentsGravatar herbelin2001-04-25
* Bug affichage ordre des variables d'un patternGravatar herbelin2001-04-15
* Mise en place d'un test de clauses non utiliseesGravatar herbelin2001-04-13
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* Alias suite + bugs divers et variésGravatar herbelin2001-03-14
* Rien au lieu erreur si plusieurs cas par défaut; quasi-achèvement alias dé...Gravatar herbelin2001-03-12