aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init/Logic.v
Commit message (Expand)AuthorAge
* Switched to "standardized" names for the properties of eq andGravatar herbelin2009-01-01
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
* - Optimized "auto decomp" which had a (presumably) exponential inGravatar herbelin2008-12-26
* Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic.Gravatar emakarov2007-11-08
* Révision de theories/Logic concernant les axiomes de descriptions.Gravatar herbelin2007-10-03
* Ajout infos de débogage de "universe inconsistency" quand option SetGravatar herbelin2007-09-30
* Mise en forme des theoriesGravatar notin2006-10-17
* Passage à une définition de inhabited plus dans les 'standard mathématique...Gravatar herbelin2006-08-28
* Modification déf de exists! pour éviter une éta-expansion et pouvoir être...Gravatar herbelin2006-06-09
* Remplacement 'singleton' par 'unique' as a simple way to avoid a conflict wit...Gravatar herbelin2006-06-04
* Ajout exists! et restructuration/extension des fichiers sur laGravatar herbelin2006-06-04
* Modification des propriétés (svn:executable)Gravatar notin2006-03-17
* Titres moins envahissants pour coqdocGravatar herbelin2006-03-04
* Ajout 'exists! x:A, P (suite)Gravatar herbelin2006-02-23
* Ajout 'exists! x:A, PGravatar herbelin2006-02-23
* code mortGravatar herbelin2006-02-10
* Correction associativité de IF et exists (visible à l'affichage uniquement ...Gravatar herbelin2006-01-19
* Contrepartie de la suppression des boites automatiques dans formatGravatar herbelin2005-12-22
* DocumentationGravatar herbelin2005-05-19
* Nouvelle en-têteGravatar herbelin2004-07-16
* CommentairesGravatar herbelin2004-03-29
* MAJ CommentairesGravatar herbelin2004-02-28
* Commentaires en v8Gravatar herbelin2004-01-09
* Finalement, espacement autour du ':' pour a la fois exists, forall et funGravatar herbelin2003-12-23
* Affichage sur le modèle du forall pour le existsGravatar herbelin2003-12-21
* modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesGravatar barras2003-12-15
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Automatisation de la traduction de iff_trans; renommage IFGravatar herbelin2003-11-14
* reorganisation des niveaux (ex: = est a 70)Gravatar barras2003-10-22
* Maintenant avant DatatypesGravatar herbelin2003-10-21
* Des implicites plus 'naturels' pour eq_ind, identity_ind and coGravatar herbelin2003-10-17
* Changement 'as notation' en 'where notation'Gravatar herbelin2003-10-14
* mise a jour nouvelle syntaxeGravatar barras2003-10-11
* type_scopeGravatar herbelin2003-10-10
* Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...Gravatar herbelin2003-09-23
* Concentration des notations officielles dans Init/Notations; restructuration ...Gravatar herbelin2003-05-21
* Activation des implicites pour la v8Gravatar herbelin2003-04-09
* eq fusionne avec eqT et devient par défaut sur Type,Gravatar herbelin2003-03-29
* Généralisation de l'utilisation de NotationGravatar herbelin2002-11-24
* option -dump-glob pour coqdocGravatar filliatr2002-02-14
* modification de la definition des def inductives unitaires et autorisation d'...Gravatar mohring2002-01-29
* MAJ des Id pour coqwebGravatar herbelin2002-01-09
* Suppression d'Export redondantsGravatar herbelin2001-11-14
* TransparentGravatar barras2001-09-20
* ajout option , Exc --> option, et lemmes dans les theoriesGravatar mohring2001-08-29
* Expérimentation de NewDestruct et parfois NewInductionGravatar herbelin2001-08-05
* entetesGravatar filliatr2001-03-15
* separation calcul des implicites et declaration des constantes / inductifs / ...Gravatar filliatr2000-11-21
* fichiers prelude CoqGravatar filliatr1999-12-13