aboutsummaryrefslogtreecommitdiff
path: root/states
AgeCommit message (Collapse)Author
2012-08-23No more states/initial.coq, instead coqtop now requires Prelude.voletouzey
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
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
2009-03-04removed unused state filebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11961 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵notin
'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 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
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@5032 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10MAJ .v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4574 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-25Logic_TypeSyntax a disparuherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4476 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
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
2003-03-14*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3771 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-09branchement extraction en standard (pas de Require)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1561 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-06EqDecidefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1336 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-02Portage d'AutoRewritedelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1043 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-20portage Refinefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@559 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-21portage EAuto et Ringfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@513 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-05ajout d'Inversionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@429 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-20Tautofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@331 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-16Syntactic Definition n'etaient pas correctemenet importeesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@320 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-21gros commit de tout ce que j'ai fait pendant les vacances :filliatr
- tactics/Equality - debug du discharge - constr_of_compattern implante vite fait / mal fait en attendant mieux - theories/Logic (ne passe pas entierrement) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@280 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-05repertoire pour les etatsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@208 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 09:32:21 +0000