aboutsummaryrefslogtreecommitdiff
path: root/theories/Logic/ClassicalDescription.v
AgeCommit message (Collapse)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-03Cleaning a little bit the files talking about descriptions: avoidingherbelin
same name for different statements as noticed by Adam Chlipala on coq-club, avoiding stating the same axiom twice in distinct files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14628 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-19- Export de pattern_ident vers les ARGUMENT EXTEND and co.herbelin
- Extension du test de réversibilité acyclique des notations dures aux notations de type abbréviation (du genre inhabited A := A). - Ajout options Local/Global à Transparent/Opaque. - Retour au comportement 8.1 pour "move" (dependant par défaut et mot-clé dependent retiré). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11472 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-15Autour du parsing:herbelin
- Utilisation de notations de type "abbreviation paramétrée" plutôt que de notations introduisant des mots-clés, là où c'est possible (cela affecte QDen, in_left/in_right, inhabited, S/P dans NZCyclic). - Extension du lexeur pour qu'il prenne le plus long token valide au lieu d'échouer sur un plus long préfixe non valide de token (permet notamment de faire passer la notation de Georges "'C_ G ( A )" sans invalider toute séquence commençant par 'C et non suivie de _) - Rajout d'un point final à certains messages d'erreur qui n'en avaient pas. - Ajout String.copy dans string_of_label ("trou" de mutabilité signalé par Georges -- le "trou" lié aux vecteurs des noeuds App restant lui ouvert). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11225 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-03Révision de theories/Logic concernant les axiomes de descriptions.herbelin
Mise à jour du tableau des axiomes dans la FAQ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10170 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-22Clarification redondance Axiome du choix unique/descriptionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9513 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-04Ajout exists! et restructuration/extension des fichiers sur laherbelin
description et le choix git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8892 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17Commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5512 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-24changement de pose en set (pose n'etait pas utilise avec la semantiquebarras
documentee). Reste a retablir la semantique de pose. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5141 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-15modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵herbelin
par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-07Biblio standard sans mention de la possibilite d'etre impredicatifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4823 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Renforcement significatif du resultat principalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4779 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Fichier offrant l'axiome du choix unique en presence de logique classiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4724 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:32:33 +0000