aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic/ClassicalFacts.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Logic library: Adding a characterization of excluded-middle in term ofGravatar Hugo Herbelin2017-03-03
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-17
|\|
| * Refine tactic now shelves unifiable holes.Gravatar Pierre-Marie Pédrot2015-12-15
* | Fix to previous commit (ClassicalFacts.v).Gravatar Hugo Herbelin2015-12-05
* | Adding proofs on the relation between excluded-middle and minimization.Gravatar Hugo Herbelin2015-12-05
|/
* Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
* Update headers.Gravatar Maxime Dénès2015-01-12
* ClassicalFacts: adds a proof that weak excluded middle implies weak proof irr...Gravatar Arnaud Spiwack2014-09-26
* A new version of Hurkens.v.Gravatar Arnaud Spiwack2014-09-24
* Updating headers.Gravatar herbelin2012-08-08
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Export de pattern_ident vers les ARGUMENT EXTEND and co.Gravatar herbelin2008-10-19
* Autour du parsing:Gravatar herbelin2008-07-15
* Ajout infos de débogage de "universe inconsistency" quand option SetGravatar herbelin2007-09-30
* TyposGravatar herbelin2007-03-15
* Mise en forme des theoriesGravatar notin2006-10-17
* Ajout exists! et restructuration/extension des fichiers sur laGravatar herbelin2006-06-04
* Modularisation des preuves concernant la logique classique, l'indiscernabilit...Gravatar herbelin2006-03-05
* Ajout étude IP généralisé, Gödel-Dummett, buveurGravatar herbelin2006-03-05
* Réponse à la conjecture que PI est indépendant de EM dans CCGravatar herbelin2004-11-02
* Nouvelle en-têteGravatar herbelin2004-07-16
* CommentairesGravatar herbelin2004-03-17
* changement de pose en set (pose n'etait pas utilise avec la semantiqueGravatar barras2003-12-24
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Biblio standard sans mention de la possibilite d'etre impredicatifGravatar herbelin2003-11-07
* Renommage bool en boolP pour eviter la qualificationGravatar herbelin2003-11-02
* Preuves dans CC deGravatar herbelin2002-08-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-21 08:34:33 +0000