aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2001-09-10Un conv aurait dû être un conv_leqherbelin
2001-09-10Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...herbelin
2001-09-09Légère modification lookup_eliminatorherbelin
2001-09-09Nettoyage reduce_to_ind et one_step_reduceherbelin
2001-09-09Passage aux univers algébriquesherbelin
2001-09-09Passage aux univers algébriquesherbelin
2001-09-09Amélioration check_module_nameherbelin
2001-09-09Préparation à la mise en place d'univers algébriquesherbelin
2001-09-09Suppression de Type_1, inutile, et non prévu dans le modèle des univers alg...herbelin
2001-09-09Préparation du prétypage à la mise en place d'univers algébriquesherbelin
2001-09-09Mécanisme pour faire remonter les contraintes de typage sur les variables de...herbelin
2001-09-09Mécanisme pour faire remonter les contraintes de typage sur les variables de...herbelin
2001-09-09Suppression du retypage dans w_Declareherbelin
2001-09-09MAJherbelin
2001-09-09Tests l'incohérence des universherbelin
2001-09-08MAJherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-24 15:50:38 +0000