aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2002-01-31changement generation de schema d'elimination, False_rec est primitif, Constr...mohring
2002-01-31extraction des CoInductives via les Lazy d'ocamlletouzey
2002-01-30cosmetiqueherbelin
2002-01-30ajout list_split3, pr_semicolon et pr_barherbelin
2002-01-30Reparation erreur de syntaxemohring
2002-01-29modification de la definition des def inductives unitaires et autorisation d'...mohring
2002-01-29condition de positivite moins stricte vis-a-vis des parametres (cf bug de Edu...barras
2002-01-25Test affichage O de nat dans une expression sur Zherbelin
2002-01-25Bug affichage de O (de nat) dans une expression sur Zherbelin
2002-01-25*** empty log message ***herbelin
2002-01-25Zdiv et Zmod dans Zcomplementsfilliatr
2002-01-25patch Omega (bug 129)filliatr
2002-01-25Correction bug 'Check [b]if b then O else O'herbelin
2002-01-25Remplacement cut_intro par true_cut_anon pour Inversionherbelin
2002-01-25Bug calcul de la signature incorrecte en présence de letinherbelin
2002-01-24Correction de l'ordre des open (sachant que de toutes façons, unherbelin
2002-01-24Remplacement cut_intro par true_cut_anonherbelin
2002-01-24Bug calcul de la signature incorrecte en présence de letinherbelin
2002-01-24code mortherbelin
2002-01-24Cas LetIn superflu dans check_construct car normalisation préalableherbelin
2002-01-24Bug dépendances en les corps des let-in oubliéesherbelin
2002-01-24Réparation bug 'known_dependent'herbelin
2002-01-23In Pcoq, the search commands had an erroneous behavior. Bound variablesbertot
2002-01-23paquet Debian 7.2-3courant
2002-01-21mise a jourfilliatr
2002-01-21warning en mode verbeux seulementfilliatr
2002-01-21Correction de Pierre Crégut pour le bug MERGE_EQherbelin
2002-01-21Ajout test de Pierre Crégutherbelin
2002-01-21Zinv -> Zoppfilliatr
2002-01-18*** empty log message ***herbelin
2002-01-18*** empty log message ***herbelin
2002-01-18Bug MERGE_EQherbelin
2002-01-18Bug commentaire (*i i*)herbelin
2002-01-18Pas d'assert false dans un try with !herbelin
2002-01-18amadouage de coqwebletouzey
2002-01-18Plusieurs arguments autorisés pour Require et Read Moduleherbelin
2002-01-18Plusieurs arguments autorisés pour Require et Read Module; mise en place d'u...herbelin
2002-01-18List.map avec ordre des effets de bord garantiherbelin
2002-01-18Le chargement des coercions est nécessaire même si le module n'est pas ouvertherbelin
2002-01-18code redondant avec is_verboseherbelin
2002-01-18modifs ZArith & Chineseletouzey
2002-01-18ajouts provenant de Chinese dans ZArith + deplacements de 3 fichiers de contr...letouzey
2002-01-18*** empty log message ***courant
2002-01-17MAJherbelin
2002-01-17Amélioration affichage échec lookup_eliminatorherbelin
2002-01-17MAJherbelin
2002-01-16correction de bug avec les mutuels imbriques a plusieurs niveauxbarras
2002-01-16Ajout d'un test sur les anonymes dépendant dans des arguments implicitesherbelin
2002-01-16Correction d'un problème avec les motifs anonymes dépendant dans des argume...herbelin
2002-01-15MAJherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-23 03:09:41 +0000