aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-09-26Induction -> NewInduction; '++' pour appherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4483 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Nouvelle serie de traductionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4482 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Re-possibilite changement chaine infixe en passant v7 a v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4481 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Passage de Destruct a NewDestruct; '-' pour negbherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4480 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Structuration de fast_integer en operations sur positive, proprietes des ↵herbelin
operations sur positive, operations sur Z, proprietes des operations sur Z; suppression section; true_sub devient definition git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4479 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Un peu plus de souplesse dans la globalisation des noms utilises par les ↵herbelin
tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4478 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Decouplage printing en v8 pour les interpretations de notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4477 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-09-25add_x_x de fast_integer vers auxiliaryherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4475 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-25Retour provisoire a une sectionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4474 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-25V8Infix declarait a tort une regle d'interpretation V7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4473 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-24Passage options via COQFLAGS plutot que OPTherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4472 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-24Traduction aussi si -translate et -load-vernac-sourceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4471 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-24Suppression section, ce qui evite de repliquer les declarations d'Infixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4470 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-24Destruct/Induction -> NewDestruct/NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4469 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-24Destruct -> NewDestructherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4468 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-24Utilisation de noms dans 'Implicit Arguments [...]'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4467 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-24majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4466 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Remplacement de Induction/Destruct par NewInduction/NewDestructherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4465 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Remplacement de Induction/Destruct par NewInduction/NewDestructherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4464 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Remplacement de Induction/Destruct par NewInduction/NewDestructherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4463 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Correction bug NewInduction pour les inductifs de type 'ordinaux'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4462 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Fusion des fichiers de syntaxe de Init avec les fichiers de définition; ↵herbelin
TypeSyntax inutile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4461 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Fonctions utilesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4460 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Utilisation de noms dans 'Implicit Arguments [...]'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4459 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Changement de l'afficheur pour que les variables liées aient un nom ↵herbelin
indépendant des globaux quand hors but (on garde l'évitement des globaux en but, pour compatibilité) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4458 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Ajout fonctions syntaxe v8 pour contrib MapleModeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4457 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Correction bug 328coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4456 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23test d'implicite incorrect depuis que eq porte sur Typebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4455 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Bug internalisation des Extern: la globalisation doit etre stricteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4453 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4452 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22commit accidentel d'une bidouilleletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4451 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22traducteur: affiche les commentaires a l'interieur des commandesbarras
extraction: pb avec les variables de section definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4450 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22L'exemple phare de modules - simplifie pour TPHOLscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4449 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4448 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22Anglaisherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4447 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22Système de renommage des noms de tactiques Ltacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4446 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22Bug d'externalisation des constantes avec uniquement des implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4445 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22suite (et fin) reparation Setoid Ringletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4444 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22typo (Benjamin, voyons ;)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4443 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22Distfix aussi adopte le nouveau schema de V8onlyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4442 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22Implicits maintenant au courant pour l'affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4441 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22Deplacement de lemmes de IntMap vers ZArithherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4440 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22tentative de rafraichissement de Setoid Ringletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4439 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22message d'erreur de garde des cofixbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4438 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22Passage à la V8 par défautherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4437 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-21Renommage Implicits -> Implicitherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4436 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-21Mise en place d'implicites par noms en v8herbelin
Nouvelle list de renommage d'idents de v7 en v8 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4435 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-21Renommages divers.herbelin
Changement de la politique de V8only: V8only tout seul signifie 'seulement interprétation' en V8; héritage des paramêtres de V7 seulement si pas V8only; sinon, il faut tout expliciter (pas d'héritage partiel) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4434 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-21Changement de la politique de V8only: V8only tout seul signifieherbelin
'seulement interprétation' en V8; héritage des paramêtres de V7 seulement si pas V8only; sinon, il faut tout expliciter (pas d'héritage partiel) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4433 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-09 04:31:55 +0000