coq/states, branch master

No more states/initial.coq, instead coqtop now requires Prelude.vo

2012-08-23T12:52:51+00:00

 For starting a bare coqtop, the recommended option is now "-noinit"
 that skips the load of Prelude.vo. Option "-nois" is kept for
 compatibility, it is now an alias to "-noinit".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15753 85f007b7-540e-0410-9357-904b9bb8a0f7

Updating headers.

2012-08-08T18:56:15+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7

Updated all headers for 8.3 and trunk

2010-07-24T15:57:30+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7

removed unused state file

2009-03-04T19:25:43+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11961 85f007b7-540e-0410-9357-904b9bb8a0f7

Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des 'properties' de Subversion

2006-04-28T10:34:25+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7

Nouvelle en-tête

2004-07-16T20:01:26+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7

Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

2003-11-29T17:55:04+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5032 85f007b7-540e-0410-9357-904b9bb8a0f7

MAJ .v8

2003-10-10T18:54:42+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4574 85f007b7-540e-0410-9357-904b9bb8a0f7

Logic_TypeSyntax a disparu

2003-09-25T21:26:35+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4476 85f007b7-540e-0410-9357-904b9bb8a0f7

Nouvelle mouture du traducteur v7->v8

2003-08-11T10:25:04+00:00

Option -v8 à coqtop lance coqtopnew
Le terminateur reste "." en v8
Ajout construction primitive CLetTuple/RLetTuple
Introduction typage dans le traducteur pour traduire les Case/Cases/Match
Ajout mutables dans RCases or ROrderedCase pour permettre la traduction
Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts
+ Bugs ou améliorations diverses
Raffinement affichage projections de Record/Structure.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7