index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Logic
/
Eqdep_dec.v
Commit message (
Expand
)
Author
Age
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Update headers.
Maxime Dénès
2015-01-12
*
sed s'/_one_var/_on/g'
Jason Gross
2014-08-26
*
Generalize EqdepFacts
Jason Gross
2014-08-26
*
Making those proofs which depend on names generated for the arguments
Hugo Herbelin
2014-06-01
*
- Fix bug preventing apply from unfolding Fixpoints.
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Generalize eq_proofs_unicity
Jason Gross
2013-12-12
*
Improved the presentation of the proof of UIP_refl_nat.
Hugo Herbelin
2013-12-04
*
Unset Asymmetric Patterns
pboutill
2013-01-18
*
Identities over types satisfying Uniqueness of Identity Proofs
herbelin
2012-12-04
*
For the record, two examples of short proofs of uniqueness of identity
herbelin
2012-11-15
*
Updating headers.
herbelin
2012-08-08
*
Kills the useless tactic annotations "in |- *"
letouzey
2012-07-05
*
ZArith + other : favor the use of modern names instead of compat notations
letouzey
2012-07-05
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Added UIP_dec on suggestion of Eelis on #coq irc.
herbelin
2010-05-22
*
Added a few informations about file lineages (for the most part in kernel)
herbelin
2010-05-09
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
added a lemma to prove inj_pair2 when eq_dec is available.
vsiles
2007-09-26
*
Correction de 2 bugs mineurs: 1 ligne de debug oubliée dans coqdoc,
notin
2007-06-21
*
Passage de Set à Type dans Relations et Wellfounded
herbelin
2007-02-06
*
Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à
herbelin
2006-12-28
*
Mise en forme des theories
notin
2006-10-17
*
Modularisation des preuves concernant la logique classique, l'indiscernabilit...
herbelin
2006-03-05
*
Nouvelle en-tête
herbelin
2004-07-16
*
simplified proof (eq and eqT are now the same)
barras
2004-06-25
*
eq2eqT et eqT2eq devenus obsolètes
herbelin
2004-06-02
*
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...
herbelin
2003-11-29
*
Uniformisation (Qed/Save et Implicits Arguments)
herbelin
2002-04-17
*
Prise en compte des dependances dans la tactique Case
mohring
2002-03-26
*
option -dump-glob pour coqdoc
filliatr
2002-02-14
*
Ajout du paradoxe de Berardi dans Logic (preuve que EM => PI dans CCI)
barras
2001-06-18
*
Mise de (*i autour CVS info
mohring
2001-04-19
*
documentation automatique de la bibliothèque standard
filliatr
2001-04-11
*
entetes
filliatr
2001-03-15
*
Renommage des variables dans les schémas d'induction
herbelin
2001-02-14
*
caractere opaque des constantes repris en compte
filliatr
2000-12-04
*
Eqdep_dec retrouve ses noms d'origine grace au nouvel Reduction.instance util...
herbelin
2000-03-21
*
Syntactic Definition n'etaient pas correctemenet importees
filliatr
2000-03-16
*
*** empty log message ***
barras
2000-03-10
*
gros commit de tout ce que j'ai fait pendant les vacances :
filliatr
2000-01-21