aboutsummaryrefslogtreecommitdiff
path: root/theories/Logic/ClassicalEpsilon.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
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-28Fix the stdlib doc compilation + switch all .v file to utf8letouzey
1) compilation of Library.tex was failing on a "Ext_" in Diaconescu.v In fact coqdoc was trying to recognize the end of a _emphasis_ and hence inserted a bogus }. For the moment I've enclosed the phrase with [ ], but this emphasis "feature" of coqdoc seems _really_ easy to broke. Matthieu ? 2) By the way, this Library document was made from latin1 and utf8 source file, hence bogus characters. All .v containing special characters are converted to utf8, and their first line is now mentionning this. (+ killed some old french comments and some other avoidable special characters). PLEASE: let's stick to this convention and avoid latin1, at least in .v files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12363 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
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
2006-10-17Mise en forme des theoriesnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-28Passage à une définition de inhabited plus dans les 'standard ↵herbelin
mathématiques'; ajout preuve que tous les 'epsilon i P' sont égaux si P habité git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9093 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-28"Essai de remplacement de "ex P" par "exists x, P x" suite àherbelin
l'introduction d'unification de motifs à la Miller permettant une forme restreinte canonique d'unification du second ordre git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9091 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09Déplacement Int.v dans ZArith, déplacement de DecidableType.v et ↵herbelin
DecidableTypeEx.v dans Logic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8933 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@8893 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 20:43:22 +0000