aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Collapse)Author
2003-11-05Nouvelle vague de renommageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4804 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-04Extension de zarithherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4790 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Extensibilite de la grammaires des patternsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4765 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Renommage Topconstr.map_aconstr_with_binders_locherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4764 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Ajout notations pour motifs de Cases; renommage map_aconstr_with_binders_locherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4756 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Ajout CPatNotation; renommage map_aconstr_with_binders_locherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4755 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Controle par le prefixe et plus par le nom absolu pour la recherche d'objets ↵herbelin
dans la biblio standard git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4753 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-30Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ↵herbelin
associative a gauche; gestion du signe dans le parseur pas dans l'interpreteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4745 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Ajout de Print Visibilityherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4733 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-27Nouveaux renommages; mot-cle 'exists'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4717 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-21Nouveaux renommages; Traduction speciale pour 'length nil'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4693 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-21Optimisation de gen_constant_in_modulesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4689 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-21Bug Locate Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4684 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 11:52:07 +0000