aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2004-09-06bad env in mimick codebarras
2004-09-03deplacement de clenv vers pretypingbarras
2004-09-03premiere reorganisation de l\'unificationbarras
2004-08-24Expansion du prédicat du 'match' vis à vis de la dépendance en le terme fi...herbelin
2004-08-24Prise en compte expansion du prédicat du 'match' vis à vis de la dépendanc...herbelin
2004-08-24Ajout nom standard mkLambda_name pour lambda_name (et idem pour prod)herbelin
2004-08-24Deplacement des fonctions de typage des predicate de Cases a la V7 de inducti...herbelin
2004-08-23Correction bug #830 : les noms des implicites temporaires étaient inconnus a...herbelin
2004-07-16Nouvelle en-têteherbelin
2004-07-16Suppression de Rawterm.loc, branchement sur Util.locherbelin
2004-07-13bug #794: conv made in wrong envbarras
2004-07-13bug #790: better error_not_cleanbarras
2004-07-11Eta-expansion du predicat dans build_indrec (suite)herbelin
2004-07-11Eta-expansion du predicat pas seulement pour make_case mais aussi pour build_...herbelin
2004-07-11Backtrack sur l'eta-expansion systematique et incorrect du predicat du Cases ...herbelin
2004-06-30updated printing of evar context (may loop ?)corbinea
2004-06-29Essai de suppression de eta dans simpl (cf bug #779)herbelin
2004-06-28Double bug d'affichage des cases dépendants (bug #784)herbelin
2004-06-27Correction affichage v8 des records avec let (bug #798)herbelin
2004-06-25correspondance des records et noms de champs de records entre un module et sa...letouzey
2004-05-14test de conversion laissait echapper exception NotConvertiblebarras
2004-04-30Terminologie plus intuitive: evaluable -> unfoldableherbelin
2004-04-29Prise en compte d'un type dont la sorte est une evarherbelin
2004-04-27Correction incapacité à gérer les annotations de type dépendantes pour le...herbelin
2004-04-13Correction confusion entre la dependance en les termes filtrees dans l'annota...herbelin
2004-04-07bug #606: mis un message d'erreur plus clairbarras
2004-04-05Déclaration des record au chargement (ce n'est pas une question de visibilit...herbelin
2004-03-29Typoherbelin
2004-03-28Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...herbelin
2004-03-24bug de PP des fix (coqbugs #574)barras
2004-03-15preparation pour release (suite)barras
2004-03-09bug affichage des cofixbarras
2004-03-08correction de bugs des points fixesbarras
2004-03-05modif des fixpoints pour que si on donne une notation au produit, les pts fix...barras
2004-02-27Erreur de Bruijn et oubli substitution alias dans annotation du 'match'herbelin
2004-02-26Inclusion des annotations de type des filtrages dans 'Set Printing All'herbelin
2004-02-18- fixed the Assert_failure error in kernel/modopsbarras
2004-02-13Deplacement array_map_left and co dans Utilherbelin
2004-02-13Bug numerotation des occurrences pour 'simpl id at n' (suite)herbelin
2004-02-13Bug numerotation des occurrences pour 'simpl id at n' (2 protections maintena...herbelin
2004-02-05On s'affranchit de l'information inductif ou pas dans le prédicat (càdherbelin
2004-02-05Suppression des types dans la signature du predicat (ils sontherbelin
2004-02-04Reconnaissance précoce de la dépendance du prédicat en un terme filtréherbelin
2004-02-04Localisation un tout petit peu moins abstraite des erreurs de garde, mais res...herbelin
2004-02-03Relachement condition pour declarer un inductif dans la table des 'If'; contr...herbelin
2004-02-03Backtrack sur recuperation de noms a partir du type, car casse la correction ...herbelin
2004-01-29Ajout option raw_print (Set Printing All) pour desactiver toute fonctionnalit...herbelin
2004-01-29Reparation d'une rupture (en presence de types implicites) de l'invariant que...herbelin
2004-01-27Bug (destruct/induction ne savent pas traiter le cas non atomique avec paramÃ...herbelin
2004-01-12Set is not always impredicativebarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 19:58:47 +0000