aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic/Decidable.v
Commit message (Expand)AuthorAge
* Moving the Tauto tactic to proper Ltac.Gravatar Pierre-Marie Pédrot2016-02-22
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* A decidability property of functional relations over decidable codomains.Gravatar herbelin2012-11-15
* Updating headers.Gravatar herbelin2012-08-08
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
* factorization part II (Properties + EqProperties), inclusion of FSetDecide (f...Gravatar letouzey2008-02-02
* Nouvelle en-têteGravatar herbelin2004-07-16
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Uniformisation (Qed/Save et Implicits Arguments)Gravatar herbelin2002-04-17
* option -dump-glob pour coqdocGravatar filliatr2002-02-14
* Mise de (*i autour CVS infoGravatar mohring2001-04-19
* Ajout lemmes arithmetiquesGravatar mohring2001-04-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 22:42:57 +0000