aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-01-20MAJherbelin
2003-01-20Petits bugsherbelin
2003-01-19Tests ltacherbelin
2003-01-19Il ne doit plus y avoir de preuves non terminées à la sortie du fichierherbelin
2003-01-19Simplification de Simplify (plus de ())herbelin
2003-01-19MAJ Ltacherbelin
2003-01-19Utilisation d'une exception 'catchable'herbelin
2003-01-19Clear sur hypothese non definieherbelin
2003-01-19Restructuration interpréteur de tactique: plus d'évaluation partielle à la...herbelin
2003-01-19Restructuration interpréteur de tactique: plus d'évaluation partielle à la...herbelin
2003-01-19Ajout pptacherbelin
2003-01-19Erreur sur precedent commitherbelin
2003-01-19Restructuration interpréteur de tactique: plus d'évaluation partielle à la...herbelin
2003-01-19Localisationherbelin
2003-01-19Rétablissement pr_patternherbelin
2003-01-18majfilliatr
2003-01-17msg Failtac; echec -batch s'il reste des preuvesfilliatr
2003-01-17V7.4mohring
2003-01-17*** empty log message ***mohring
2003-01-17Version V7.4mohring
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 03:27:39 +0000