aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-09-26Syntaxe plus liberale pour le type des arguments de filtrage du 'match'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4491 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Syntaxe plus liberale pour le type des arguments de filtrage du 'match'; ↵herbelin
traduction de noms git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4490 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4489 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26pa_ifdef.cmo redondantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4488 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Ajout now_showherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4487 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26About, Infixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4486 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26'Open Local Scope' en attendant que le core_scope sache se mettre devant ↵herbelin
implicitement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4485 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Ajout 'About'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4484 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 13:54:59 +0000