aboutsummaryrefslogtreecommitdiff
path: root/theories/Logic/Eqdep_dec.v
AgeCommit message (Expand)Author
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
2002-03-26Prise en compte des dependances dans la tactique Casemohring
2002-02-14option -dump-glob pour coqdocfilliatr
2001-06-18Ajout du paradoxe de Berardi dans Logic (preuve que EM => PI dans CCI)barras
2001-04-19Mise de (*i autour CVS infomohring
2001-04-11documentation automatique de la bibliothèque standardfilliatr
2001-03-15entetesfilliatr
2001-02-14Renommage des variables dans les schémas d'inductionherbelin
2000-12-04caractere opaque des constantes repris en comptefilliatr
2000-03-21Eqdep_dec retrouve ses noms d'origine grace au nouvel Reduction.instance util...herbelin
2000-03-16Syntactic Definition n'etaient pas correctemenet importeesfilliatr
2000-03-10*** empty log message ***barras
2000-01-21gros commit de tout ce que j'ai fait pendant les vacances :filliatr