aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-01-22Commentairesdesmettr
2003-01-22Renommages dans PartSumdesmettr
2003-01-22Bug 'with Module' corrigecoq
2003-01-22Bug precedenceherbelin
2003-01-22petit bug pp haskellletouzey
2003-01-22majfilliatr
2003-01-22Extraction des modules, enfin !letouzey
2003-01-22id_of_msid en plusletouzey
2003-01-21Adaptation à la nouvelle sémantique plus uniforme de "Match term"herbelin
2003-01-21Plus du tout de backtracking dans "Match term"; vrai Exit dans débogueurherbelin
2003-01-21portabilitedoligez
2003-01-21Renommage dans MVTdesmettr
2003-01-21MAJ dans Exp_propdesmettr
2003-01-21Renommage dans Binomial.vdesmettr
2003-01-21Binome.v -> Binomial.vdesmettr
2003-01-21Binome.v -> Binomial.vdesmettr
2003-01-21MAJ ArithPropdesmettr
2003-01-21Renommage dans AltSeries.vdesmettr
2003-01-21Renommage dans Alembert.vdesmettr
2003-01-21Quelques améliorationsdesmettr
2003-01-21Suppression de INR2 / Conséquence logique de la nouvelle représentation des...desmettr
2003-01-21Quelques optimisations...desmettr
2003-01-21Make sure pcoq will also display hypotheses with a value.bertot
2003-01-21Add a few operators in the new version of xlate.ml and make surebertot
2003-01-21majfilliatr
2003-01-20Mauvaise interprétatin de IdentArgTypeherbelin
2003-01-20Cgt définition de platdesmettr
2003-01-20Amélioration de DiscrRdesmettr
2003-01-20*** empty log message ***herbelin
2003-01-20Protection contre les noms de tactiques inconnus; restriction exceptions ratt...herbelin
2003-01-20Utilisation de 'Recursive' pour les tactiques récursivesherbelin
2003-01-20deplacement du test 'il reste des preuves en cours'filliatr
2003-01-20Utilisation de 'Recursive' pour les tactiques récursivesherbelin
2003-01-20majfilliatr
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 10:30:11 +0000