aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2001-06-15Fix d'un bug de Tautodelahaye
2001-06-13plus besoin de separer les ?barras
2001-06-13Prise en compte env local (et defs locales) dans Changeherbelin
2001-06-12Ajout d'une normalisation (beta_iota) pour les predicats de Cases inferes aut...clrenard
2001-06-12Ajout des entrees puor Setoid_replace.clrenard
2001-06-12Ajout de la tactique Setoid_replace.clrenard
2001-06-11Reparation d'un bug d'affichage. Les let destructurants, if, et vieux Caseclrenard
2001-06-11Fix de quelques bugs syntaxiques de Ltacdelahaye
2001-06-05Ajout de deux anciens bugsdelahaye
2001-06-04Correction bug outsidemayero
2001-06-01Correction d'un bug du a un Intros trop violentdelahaye
2001-06-01Backtrack vers comportement de la V6 pour eviter les globaux dans le nommage ...herbelin
2001-05-31Creation du fichier Zhints.v repertoriant les thms de ZArith et definissant l...herbelin
2001-05-31Amelioration - subjective - de l'affichage des Hintherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 21:51:17 +0000