aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2001-09-07MAJherbelin
2001-09-07Extension à Cases et Fix de la réduction pas à pas vers un produit (Red)herbelin
2001-09-07Suppression des library roots, on teste si un nom est absolu autrementherbelin
2001-09-06Rétablissement de Print Sectionherbelin
2001-09-06MAJherbelin
2001-09-06Bug default module name (2eme)herbelin
2001-09-06Bug default module nameherbelin
2001-09-05Version de la reduction dans Closure plus econome en memoire:barras
2001-09-04Nouveau coq.spec avec les droits de rootherbelin
2001-09-04erreur de pretty-print lors de l'affichage de termes avec de Bruijn non liesbarras
2001-09-03Correction d'un bug de pretty-print.clrenard
2001-08-31prise en compte de Load par coqdepfilliatr
2001-08-30Fin de la modif Exc/optionmohring
2001-08-29ajout option , Exc --> option, et lemmes dans les theoriesmohring
2001-08-28Change la constante d'entree de Immediatemohring
2001-08-28Remplace numarg -> pure_numarg dans Double Inductionmohring
2001-08-28remplace numarg -> pure_numargmohring
2001-08-13Rétablissement nom de section Map après résolution bugs surcharge de nomsherbelin
2001-08-13Protection des commentaires pour coqtex et coqwebherbelin
2001-08-13bug de Bruijnherbelin
2001-08-13bug incompatibilitéherbelin
2001-08-10Pour contourner un bug de camlp4 3.02herbelin
2001-08-10Hack rapide pour réduire significativement la taille des voherbelin
2001-08-10Bugherbelin
2001-08-10Prsingherbelin
2001-08-10Prise en compte des strings et des flottants dans les statistiques de tailles...herbelin
2001-08-10Parsingherbelin
2001-08-10Repository : pauillac.inria.fr:/net/pauillac/constr/ARCHIVEherbelin
2001-08-08Renommage TrueCut -> Assertherbelin
2001-08-08Ajout nf_betaiota dans le cut interneherbelin
2001-08-08La grammaire n'était plus LL1herbelin
2001-08-08Modification Tauto pour qu'il puisse destructurer des hypotheses de la formecourant
2001-08-07Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...herbelin
2001-08-07Passage au nouveau Destructherbelin
2001-08-06Nouvelle entrée ident_or_numargherbelin
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
2001-08-05Code mortherbelin
2001-08-05Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas s'a...herbelin
2001-08-05Elimination des coupures quand les 'clause' se réduisent à des hypothèses,...herbelin
2001-08-05Ajout error_global_not_foundherbelin
2001-08-05Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas s'a...herbelin
2001-08-05Mise en place d'un nouveau Destruct sur le modèle du nouvel Inductionherbelin
2001-08-05Suppression des TmpHyp disgracieuses dans Decompose; utilisation de combinate...herbelin
2001-08-05Elimination des coupures quand les 'clause' se réduisent à des hypothèses,...herbelin
2001-08-05Nouveau profiler compatible avec ocaml >= 3.01herbelin
2001-08-01Ajout code pour un Destruct similaire au NewInductionherbelin
2001-08-01Ajout make_elimination_identherbelin
2001-08-01Ajout add_prefix/add_suffixherbelin
2001-08-01Ajout profile dans PARSERREQUIRE, nécessaire si certaines fonctions d'un des...herbelin
2001-08-01MAJ vis à vis de ocaml 3.01herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 03:16:04 +0000