index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
theories
/
Logic
/
Eqdep_dec.v
Age
Commit message (
Expand
)
Author
2009-09-17
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2007-09-26
added a lemma to prove inj_pair2 when eq_dec is available.
vsiles
2007-06-21
Correction de 2 bugs mineurs: 1 ligne de debug oubliée dans coqdoc,
notin
2007-02-06
Passage de Set à Type dans Relations et Wellfounded
herbelin
2006-12-28
Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à
herbelin
2006-10-17
Mise en forme des theories
notin
2006-03-05
Modularisation des preuves concernant la logique classique, l'indiscernabilit...
herbelin
2004-07-16
Nouvelle en-tête
herbelin
2004-06-25
simplified proof (eq and eqT are now the same)
barras
2004-06-02
eq2eqT et eqT2eq devenus obsolètes
herbelin
2003-11-29
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...
herbelin
2002-04-17
Uniformisation (Qed/Save et Implicits Arguments)
herbelin
2002-03-26
Prise en compte des dependances dans la tactique Case
mohring
2002-02-14
option -dump-glob pour coqdoc
filliatr
2001-06-18
Ajout du paradoxe de Berardi dans Logic (preuve que EM => PI dans CCI)
barras
2001-04-19
Mise de (*i autour CVS info
mohring
2001-04-11
documentation automatique de la bibliothèque standard
filliatr
2001-03-15
entetes
filliatr
2001-02-14
Renommage des variables dans les schémas d'induction
herbelin
2000-12-04
caractere opaque des constantes repris en compte
filliatr
2000-03-21
Eqdep_dec retrouve ses noms d'origine grace au nouvel Reduction.instance util...
herbelin
2000-03-16
Syntactic Definition n'etaient pas correctemenet importees
filliatr
2000-03-10
*** empty log message ***
barras
2000-01-21
gros commit de tout ce que j'ai fait pendant les vacances :
filliatr