aboutsummaryrefslogtreecommitdiff
path: root/theories/Logic/Eqdep_dec.v
AgeCommit message (Expand)Author
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2007-09-26 added a lemma to prove inj_pair2 when eq_dec is available.vsiles
2007-06-21Correction de 2 bugs mineurs: 1 ligne de debug oubliée dans coqdoc, notin
2007-02-06Passage de Set à Type dans Relations et Wellfoundedherbelin
2006-12-28Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type àherbelin
2006-10-17Mise en forme des theoriesnotin
2006-03-05Modularisation des preuves concernant la logique classique, l'indiscernabilit...herbelin
2004-07-16Nouvelle en-têteherbelin
2004-06-25simplified proof (eq and eqT are now the same)barras
2004-06-02eq2eqT et eqT2eq devenus obsolètesherbelin
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
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