aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Collapse)Author
2003-10-21Deplacement de Ppvernacnew.pr_reference dans Ppconstrnew pour utilisation ↵herbelin
par Pptactic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4694 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-21Extension de Locateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4688 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-17On n'autorise plus les niveaux doubles L/R en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4670 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-17Bug mot-cle TYPESherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4667 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-17Traduction des idents aussi dans le printer generique des tactiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4664 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16nouvelle syntaxe de ltacbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4661 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16lettac -> setbarras
suppression de la notation carre de R git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4659 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16Bug Searchherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4644 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-15Mise en conformite return_type en fonction de la docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4643 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-14Changement 'as notation' en 'where notation'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4632 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Ameliration affichage inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4615 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Ajout d'une fonction de recherche sur les composantes du nom des objetsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4613 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Ajout d'une fonction de recherche sur les composantes du nom des objetsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4608 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-11Ajout fnl() dans Aboutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4599 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-11mise a jour nouvelle syntaxebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4595 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Suppression Grammar/Syntaxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4593 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Delimiters N devient 'nat'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4579 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Cablage en dur de inversionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4566 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-09Compatibilite ocaml 3.06 et 3.07herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4554 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé ↵herbelin
incomplètement prouvé comme axiome git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4543 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Essai de traduction du contraire de 'tacledit bin/coqtop.byte' en 'tac...'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4537 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Debranchement de l'affichage automatique de Proof par le traducteur (trop ↵herbelin
complique de trouver la bonne indentation); affichage en revanche de Proof s'il existait deja git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4536 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Inspect saute maintenant les marqueurs invisiblesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4535 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-02Hypothesis mot-cleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4515 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-01Implantation de l'option 'format' des Notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4509 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-30Les notations hors scope s'empilent maintenant comme des scopes neherbelin
contenant qu'une notation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4503 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-30Ajout 'Close Scope'.herbelin
Mise en place de la structure pour un modificateur 'format' de Notation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4502 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Bug aboutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4492 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-26Ajout 'About'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4484 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-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-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-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-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-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
2003-09-21Parsing au niveau lconstr des patterns de 'match context'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4432 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-19Mise en place des V8Notation et V8Infix pour déclarer des notations enherbelin
v8 même si incompatible avec la syntaxe v7 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4419 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-18Ajout r gle d'affichage tactiques èéfinies par Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4409 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-18Simplification afficheur de tactiques non primitiveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4408 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-16En attendant l'afficheur...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4405 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et ↵herbelin
choix du parseur en fonction de cette option git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4387 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Fusion des g_*syntaxnew.ml avec les g_*syntax.ml avec sélection dynamique selonherbelin
l'option v7 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4385 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Ajout 'Print Scopes' et 'Bind Scope with classes'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4378 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12MAJ module requis pour le parsing des numérauxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4377 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Affichage des scopes d'argumentsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4376 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-24 18:50:43 +0000