coq/theories7, branch master The formal proof system Suppression des fichiers .v en ancienne syntaxe 2005-12-26T13:59:13+00:00 herbelin 2005-12-26T13:59:13+00:00 f6e1acbbe00aeb479fde229c3941e3a6a2d53068 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7733 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7733 85f007b7-540e-0410-9357-904b9bb8a0f7
Détection d'un Fold incorrect suite à correction bug #986 2005-07-13T23:43:54+00:00 herbelin 2005-07-13T23:43:54+00:00 1cfbf3408b8d7d452233b31fbdc2e0b98821c213 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7223 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7223 85f007b7-540e-0410-9357-904b9bb8a0f7
Explicitation d'un nom de variable nécessaire au bon typage, suite à suppression des _ du contexte des evars 2005-03-12T15:56:26+00:00 herbelin 2005-03-12T15:56:26+00:00 be2ee6dc08ec3cbfb04cdd4b8ecc2b5326805893 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6829 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6829 85f007b7-540e-0410-9357-904b9bb8a0f7
Tactics.v bidon pour accomoder make world7 2005-02-03T17:15:03+00:00 herbelin 2005-02-03T17:15:03+00:00 554e424105641b9051b4a7cee069f5584c22074a git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6671 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6671 85f007b7-540e-0410-9357-904b9bb8a0f7
Généralisation à Type de certaines propriétés des relations 2004-11-19T22:12:33+00:00 herbelin 2004-11-19T22:12:33+00:00 b22125319bf7ba65b0c5ce00124285351277895a git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6331 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6331 85f007b7-540e-0410-9357-904b9bb8a0f7
'match term' now evaluates by default. Added 'lazy' keyword to delay the evaluation of tactics 2004-10-11T11:39:18+00:00 herbelin 2004-10-11T11:39:18+00:00 56ab825d3fbcd1d517027875245d1cafda68a6dc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6199 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6199 85f007b7-540e-0410-9357-904b9bb8a0f7
V7 .v files for Setoid_* and Ring over setoids commented out. 2004-09-03T09:27:26+00:00 sacerdot 2004-09-03T09:27:26+00:00 c0d7769b366e387ed9e00b05870991c4c9440f41 To re-enable them I would need to back-port theories/Setoids/Setoid.v from the new syntax to the old syntax. However, since the translator is going to be removed from the next major Coq version, I am not doing it (unless required to). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6046 85f007b7-540e-0410-9357-904b9bb8a0f7 
To re-enable them I would need to back-port theories/Setoids/Setoid.v from the
new syntax to the old syntax. However, since the translator is going to
be removed from the next major Coq version, I am not doing it (unless
required to).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6046 85f007b7-540e-0410-9357-904b9bb8a0f7
Nouvelle en-tête 2004-07-16T20:01:26+00:00 herbelin 2004-07-16T20:01:26+00:00 763cf4f37e10d9a0e8a2a0e9286c02708a60bf08 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
Bug réaffichage EXT 2004-04-15T15:53:21+00:00 herbelin 2004-04-15T15:53:21+00:00 7ffd9e720a7e615bd5a55c9e1a6674d3b69ba177 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5678 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5678 85f007b7-540e-0410-9357-904b9bb8a0f7
Definition de la notation de la paire par un motif recursif 2004-03-17T11:28:04+00:00 herbelin 2004-03-17T11:28:04+00:00 f97b4b1e33fba9577b8a7a92a5c01b2ca10451f6 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5519 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5519 85f007b7-540e-0410-9357-904b9bb8a0f7