aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-01-17Mise a jour pour distribmohring
2003-01-17*** empty log message ***mohring
2003-01-17Optimisations pour Sup et RComputedesmettr
2003-01-17majfilliatr
2003-01-16Bugs affichageherbelin
2003-01-16*** empty log message ***herbelin
2003-01-16Subst sur une hyp qui n'existe pas ne fait pas une anomaliebarras
2003-01-16Ajout de RComputedesmettr
2003-01-16Ajout de la tactique Supdesmettr
2003-01-16*** empty log message ***desmettr
2003-01-16renommage de TAF.v en MVT.vdesmettr
2003-01-16-emacs: plus de prompt entre les lignesfilliatr
2003-01-16Correction d'un petit bug dans Sup0desmettr
2003-01-16Renommage de RealsB en Rbasedesmettr
2003-01-16Renommage de Rbase.v en RIneq.vdesmettr
2003-01-16majfilliatr
2003-01-15Problème de désynchronisation des variables du type et du corps d'un point-...herbelin
2003-01-15Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...herbelin
2003-01-15Bug en présence de let-inherbelin
2003-01-15Nouvelle interprétation des nombres réelsdesmettr
2003-01-15Bug en présence de let-inherbelin
2003-01-15Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...herbelin
2003-01-13patch configure (V Aymeric)filliatr
2003-01-10majfilliatr
2003-01-09Export M + Module M <: SIGcoq
2003-01-09correction de bug de Subst: ne faisait rien lorsque l'hypothesebarras
2003-01-08majfilliatr
2003-01-07Retour printer ast pour V7.4herbelin
2003-01-07majfilliatr
2003-01-06SearchAboutfilliatr
2003-01-06bit vectorsfilliatr
2002-12-31Amélioration règles d'affichageherbelin
2002-12-30Commentaires; optimisationherbelin
2002-12-30Amélioration choix des noms dans abstract_list_allherbelin
2002-12-28Prise en compte notations dans les extensions de motiffherbelin
2002-12-28Re-installation nombres dans les motifs sur Zherbelin
2002-12-24Utilisation du second-ordre avec possibilité de K-rédex dans lemInvherbelin
2002-12-24code mortherbelin
2002-12-23Re-essai de forcer le terme réécrit à apparaître dans le butherbelin
2002-12-23Tentative d'interdire les K-abstractions si allow_K est faux et leherbelin
2002-12-23Prise en compte application partielle dans dependentherbelin
2002-12-23majfilliatr
2002-12-22Cas motif universelherbelin
2002-12-21Backtrack sur la tentative d'interdire les K-abstractions dans l'unificationherbelin
2002-12-21Légère amélioration des messages d'erreur des with-bindings et des Rewriteherbelin
2002-12-21Affinement affichageherbelin
2002-12-21code mortherbelin
2002-12-21Affinement affichageherbelin
2002-12-21Plus de notation cablees dans 'annot'herbelin
2002-12-21majfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 16:18:06 +0000