aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2001-07-10anomaly -> errorclrenard
2001-07-09MAJ de la MAJherbelin
2001-07-09MAJherbelin
2001-07-09Backtrack sur le warning Require en Section: trop contraignantherbelin
2001-07-06Les tables de coercions ne doivent pas survivre aux sectionsherbelin
2001-07-06la conversion ne doit être testé dans evar_conv qu'en absence de evarherbelin
2001-07-06has_undefined_isevars était buggéherbelin
2001-07-06version 7.0+1 (pour Nicolas Magaud)filliatr
2001-07-05Avertissement contre les Require dans le corps d'une sectionherbelin
2001-07-05Interdiction de faire 2 variables de même nom courtherbelin
2001-07-05Débogage discharge des coercions; nettoyageherbelin
2001-07-05correction bug Omegafilliatr
2001-07-04ajout Show Intro(s)letouzey
2001-07-04message Ambiguous paths seulement si verbosefilliatr
2001-07-03Ajout hashconsing universherbelin
2001-07-03Depliage des let-in dans le test de gardeherbelin
2001-07-02Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute...herbelin
2001-07-02Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute...herbelin
2001-07-02Nettoyage/restructuration des ensembles d'indicateurs de réductionsherbelin
2001-07-02Ajout glob_eq{,T}herbelin
2001-06-29Autoriser Apply avec un but sous forme d'implication ou de quantificationbarras
2001-06-29Backtracking pour le Matchdelahaye
2001-06-29traitement du let dans red_product (tactique Red)barras
2001-06-27commit d'un bug de Apply.barras
2001-06-27Reduction du terme preuve fourni par Fielddelahaye
2001-06-27correction d'un bug de Correctness (pour Y Bertot)filliatr
2001-06-27Reduction tres significative du terme preuvedelahaye
2001-06-26Les tacticques Setoid_replace/rewrite peuvent maintenant reecrire sous uneclrenard
2001-06-26Mise a jour des .dependclrenard
2001-06-25Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...herbelin
2001-06-25Refine sur les CoFixfilliatr
2001-06-25Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...herbelin
2001-06-25Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...herbelin
2001-06-25Bug inférence du prédicat en présence de K-rédexherbelin
2001-06-25Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...herbelin
2001-06-25liste des equiv exporteeclrenard
2001-06-25Bug dépendances non pertinentes (dû à des K-rédex) dans le type des branc...herbelin
2001-06-222 bugs: typevarlist pour inductifs + args pour flexiblesletouzey
2001-06-20Ajout d'un Setoid_rewrite et meilleure resolution des petits sous-buts géné...clrenard
2001-06-20Normalisation du predicat synthetise pour les Caseclrenard
2001-06-20oubli de Elimdep dans le Makefilebarras
2001-06-19Un bug corrige.clrenard
2001-06-19Ajouts des theories du paradoxe de Berardidelahaye
2001-06-19Extension des parametres de Clear + Instdelahaye
2001-06-19Extension des parametres de Cleardelahaye
2001-06-19Oubli Save + je sais plusmayero
2001-06-18Ajouts de lemmes (pour Float)mayero
2001-06-18Ajout du paradoxe de Berardi dans Logic (preuve que EM => PI dans CCI)barras
2001-06-18Interpretation MetaId + Progress + Instdelahaye
2001-06-16code mortherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-25 12:54:14 +0000