aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Collapse)Author
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
2003-08-11Ajout LetTupleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4260 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-06-10Ajout notation c.(f) en v8 pour les projections de Recordherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4128 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Déplacement traducteur de nom dans Constrextern pour accès aux noms longsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4126 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Amélioration afficheur de Cases pour les constr_patternherbelin
Déplacement traducteur de nom dans Constrextern pour accès aux noms longs Extension du traducteur de nom Ajout notation c.(f) en v8 pour les projections de Record git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4117 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Extension de Locate sur les symboles avec recherche de sous-chaînes; mise ↵herbelin
en place structure pour des 'arguments scope' dirigés par une classe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4109 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4054 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ↵herbelin
les metavariables de patterns; fusion NoHypId et Hyp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4043 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Restructuration des procédures de filtrageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4032 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-14Hack pour ameliorer l'affichage des applications dans les `...` etherbelin
``...`` en les mettant sous forme n-aire, et sans casser la compatibilite des implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4018 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-29Prise en compte des syntaxes v8 dans Uninterpreted Notationherbelin
Suite mise en place infrastructure pour déclaration de syntaxe simultanée à la déclaration d'inductifs Table séparée pour les précédences de notations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3983 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-17Ajout "at next level" dans Notationherbelin
Mise en place structure pour définir un objet en même temps que sa notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3939 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-16simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = ↵letouzey
list_skipn n l git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3931 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-16On force l'affichage des implicites non '?' lors de la traductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3926 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-15Affichage coercions en mode -(f)translateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3924 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-11Ajout option 'Local' à Infix et Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3915 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10Affichage forcé des implicites contextuels si pas de contexte connuherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3910 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10Relachement globalisation Unfold en usage interactifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3907 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Mécanisme plus simple et efficace pour traduire les implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3889 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Réorganisation de Impargs + mise en place d'une infrastructureherbelin
(notatemment des tables de parsing et d'affichage différenciées) permettant au traducteur de changer les implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3874 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-08Application de l'absence d'export aux modulesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3869 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-08En-tete docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3868 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-08Ajout option "Local" à "Open Scope"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3867 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3857 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Stratégie d'affichage des coercions plus défensive (mais pas très optimale)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3856 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Suppression des explicitations d'implicite inutilesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3848 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-01Déplacement with_option dans Optionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3835 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 05:56:51 +0000