aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Collapse)Author
2003-10-17Re-desactivation de l'affichage des projectionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4668 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16print_projections a true juste pour le bench nocturneherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4660 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16Message d'erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4652 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16Debranchement de l'affichage systematique des projections avec la notation ↵herbelin
pointee; soumis maintenant a l'activation de l'option 'Set Printing Projections' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4651 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16Debranchement de l'affichage systematique des projections avec la notation ↵herbelin
pointee; soumis maintenant a l'activation de l'option 'Set Printing Projections' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4649 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-15Gestion encore plus affinee des implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4641 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-14Gestion affinee des implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4637 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-14Nouvelles traductions de noms; mot-cle; affichage implicites par le traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4636 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-14identityT = identityherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4633 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-14Plus d'uniformite dans la gestion des implicites d'inductifs; nouvelles ↵herbelin
entrees pour Metasyntax git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4631 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10identity est equivalent sur Type (sauf sans argument)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4592 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10changement nouvelle syntaxe (pt fixes)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4559 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Pb residuel avec la prise en compte des parametres implicites d'inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4549 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Prise en compte des paramètres implicites d'inductifs pour la globalisation ↵herbelin
des types de constructeur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4548 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-01cosmetiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4510 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-30Les notations hors scope s'empilent maintenant comme des scopes neherbelin
contenant qu'une notation + renommage dans Reals git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4505 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-30code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4504 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-30Ajout 'Close Scope'.herbelin
Les notations hors scope s'empilent maintenant comme des scopes ne contenant qu'une notation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4501 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-29Prise en compte d'un inductif sans argument dans le 'in' des 'match'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4498 85f007b7-540e-0410-9357-904b9bb8a0f7
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-26Nouvelle serie de traductionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4482 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-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-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-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-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-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). Restructuration de Metasyntax. Correction bug qui cassait l'affichage de la version -translate quand utilisée en v7 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4431 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-21Mise en place d'implicites par noms en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4430 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-19parsingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4416 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-18Traduction de '_' comme referenceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4412 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-18Parsing correct des explicites en cas de projectionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4411 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Activation déclaration automatique de scope d'arguments; affichage scopes ↵herbelin
d'arguments git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4374 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Activation déclaration automatique de scope d'argumentsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4363 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Scope type pour le codomaine de Prod aussi; ajout extern_rawtypeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4360 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Scope type pour le codomaine de Prod aussiherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4359 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12open superfluherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4356 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-10Renommage des variables '_'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4350 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-10Ajout 'mod' comme keywordherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4342 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09Ajout construction If primitive dans constr_expr et rawconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4336 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09Ajout If; synchro avec constrexternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4333 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09Ajout If; renommage de l'ident '_'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4332 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Paramétrisation vis à vis de existential_keyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4321 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06cosmetiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4318 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-02Plus de passage du scope tmp sous les lambdasherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4289 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-31Symetrisation des changements implicites de scopeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4283 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-14Traducteur de correctnessherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4275 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-12Bug et améliorations diversesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4264 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 06:51:06 +0000