coq/contrib7, branch master The formal proof system Suppression des fichiers .v en ancienne syntaxe 2005-12-26T14:06:57+00:00 herbelin 2005-12-26T14:06:57+00:00 11edbc28297a9fc782d3117ea3ac7550552609fa git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7735 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7735 85f007b7-540e-0410-9357-904b9bb8a0f7
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
new congruence 2005-08-17T12:56:38+00:00 corbinea 2005-08-17T12:56:38+00:00 8cb5e072d095981aa0664ca9b6f3db8983e18437 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7298 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7298 85f007b7-540e-0410-9357-904b9bb8a0f7
Open Scope non Local malencontreux 2005-05-03T20:44:01+00:00 herbelin 2005-05-03T20:44:01+00:00 9beafe7c3fde8adfd3f9afdd74fe6842cceefe32 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6987 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6987 85f007b7-540e-0410-9357-904b9bb8a0f7
Utilisation Z_scope 2005-05-02T10:46:25+00:00 herbelin 2005-05-02T10:46:25+00:00 d4c5a863d35bb131b7236fd5df48cfc882c0b0f1 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6982 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6982 85f007b7-540e-0410-9357-904b9bb8a0f7
- changement ordre arguments interp_goal_concl pour permettre application 2005-02-21T00:38:37+00:00 herbelin 2005-02-21T00:38:37+00:00 0c52ddea0e26c5aef919aa3bf457b6e07a8871f5 partielle - amélioration traduction en nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6762 85f007b7-540e-0410-9357-904b9bb8a0f7 
  partielle
- amélioration traduction en nouvelle syntaxe


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6762 85f007b7-540e-0410-9357-904b9bb8a0f7
Passage d'une bibliothèque de grands entiers naturels vers une bibliothèques de grands entiers relatifs munis des 4 opérations de base 2004-12-24T11:25:18+00:00 herbelin 2004-12-24T11:25:18+00:00 355671c60fa075b64f64e175bada909a4ce759ac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6499 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6499 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
reals: renamed type option into field_rel_option 2004-03-11T10:26:53+00:00 marche 2004-03-11T10:26:53+00:00 db2f2ea9f22624eb6226172477b17faf87a53961 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5451 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5451 85f007b7-540e-0410-9357-904b9bb8a0f7