aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Collapse)AuthorAge
* Ajout entree pour exporter les commentaires en mode -xmlGravatar herbelin2004-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5574 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code mortGravatar herbelin2004-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5570 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hack pour traduction des changements non uniformes de syntaxe des TACTIC et ↵Gravatar herbelin2004-03-17
| | | | | | VERNAC EXTEND (e.g. Hint Rewrite) [2eme] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5526 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hack pour traduction des changements non uniformes de syntaxe des TACTIC et ↵Gravatar herbelin2004-03-17
| | | | | | VERNAC EXTEND (e.g. Hint Rewrite) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5525 85f007b7-540e-0410-9357-904b9bb8a0f7
* Parsing des V8Notation avec motif recursif en v7Gravatar herbelin2004-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5520 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation de '..' pour la notation concrete des motifs recursifs de filtrageGravatar herbelin2004-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5517 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place de motifs récursifs dans Notation; quelques simplifications ↵Gravatar herbelin2004-03-17
| | | | | | au passage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5510 85f007b7-540e-0410-9357-904b9bb8a0f7
* modif des fixpoints pour que si on donne une notation au produit, les pts ↵Gravatar barras2004-03-05
| | | | | | fixes s'affichent correctement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5435 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de noms d'entrees de grammaires qualifies dans 'Tactic Notation'Gravatar herbelin2004-03-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5426 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les ↵Gravatar herbelin2004-03-02
| | | | | | noms d'hypothèses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5419 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de natural en int_or_var pour 'do' et 'fail' pour ↵Gravatar herbelin2004-03-02
| | | | | | paramétrisation dans ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5418 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id ↵Gravatar herbelin2004-03-02
| | | | | | variable de ltac substituable dans la pratique par un intro_case_pattern dans induction, destruct et inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5415 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction oubli du cas pas d'arguments implicites du toutGravatar herbelin2004-03-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5414 85f007b7-540e-0410-9357-904b9bb8a0f7
* Généralisation du type ltac Identifier en IntroPattern; prise en compte ↵Gravatar herbelin2004-03-01
| | | | | | des IntroPattern au parsing, à l'interprétation, à la traduction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5405 85f007b7-540e-0410-9357-904b9bb8a0f7
* Expansion du type par nécessité dans le cas d'affichage d'implicitesGravatar herbelin2004-02-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5398 85f007b7-540e-0410-9357-904b9bb8a0f7
* Keep structure information for Fixpoint declaration and Fix termsGravatar bertot2004-02-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5386 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction oubli de report d'une modification de g_vernac (1.69) vers ↵Gravatar herbelin2004-02-21
| | | | | | g_vernacnew git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5371 85f007b7-540e-0410-9357-904b9bb8a0f7
* - fixed the Assert_failure error in kernel/modopsGravatar barras2004-02-18
| | | | | | | | | - fixed the problem with passing atomic tactics to ltacs - restructured the distrib Makefile (can build a package from the CVS working dir) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5358 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de lconstr, constr et binder_constr dans Print Grammar constrGravatar herbelin2004-02-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5355 85f007b7-540e-0410-9357-904b9bb8a0f7
* export the general function for getting information from the environmentGravatar bertot2004-02-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5347 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation du comportement de Notation et Reserved NotationGravatar herbelin2004-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5341 85f007b7-540e-0410-9357-904b9bb8a0f7
* Localisation des erreurs d'internalisation des notations de tactiquesGravatar herbelin2004-02-12
| | | | | | | | dans le module de leur définition. Error_in_file dans Util et étendu avec possibilité de noms de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5328 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de 'Print.' en v8Gravatar herbelin2004-01-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5265 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réutilisation de VernacSyntacticDefinition pour différencier "Notation id ↵Gravatar herbelin2004-01-29
| | | | | | | | | := c" de "Notation "'id'" := c" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5264 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout 'as (x,...,y)' dans NewDestruct et NewInd, NewInduction, ...Gravatar herbelin2004-01-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5253 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation de qqs bugs du traducteurGravatar barras2004-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5248 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection table des locations lors de Load (pour coqdoc)Gravatar herbelin2004-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5237 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export information des references et location de notations pour coqdocGravatar herbelin2004-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5228 85f007b7-540e-0410-9357-904b9bb8a0f7
* Le traducteur utilisait un afficheur des reels obsolete et buggeGravatar herbelin2004-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5221 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression 'Implicit Arguments On/Off' qui n'a plus lieu d'etre en v8Gravatar herbelin2004-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5220 85f007b7-540e-0410-9357-904b9bb8a0f7
* make libraries, lexing of more utf8 symbolsGravatar marche2004-01-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5201 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables ↵Gravatar herbelin2004-01-13
| | | | | | a b:A' et 'Variables (a:A) (b:A)' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5198 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reference obsolete au niveau 200 de patternGravatar herbelin2004-01-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5196 85f007b7-540e-0410-9357-904b9bb8a0f7
* bugs avec Pose et AssertGravatar barras2004-01-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5190 85f007b7-540e-0410-9357-904b9bb8a0f7
* meilleure presentation des commentaires du traducteurGravatar barras2004-01-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5168 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug affichage DecomposeGravatar herbelin2003-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5144 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5134 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en valeur intropattern de paires et acceptation dans le 'as' de ↵Gravatar herbelin2003-12-22
| | | | | | induction/inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5128 85f007b7-540e-0410-9357-904b9bb8a0f7
* Substitution dans REvar et PEvar plutot que encodage via noeud application ↵Gravatar herbelin2003-12-19
| | | | | | pour eviter la confusion avec la (vraie) application git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5114 85f007b7-540e-0410-9357-904b9bb8a0f7
* name_app accessible a tous dans NameopsGravatar herbelin2003-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5112 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout test de non-regression Clear d'une def localeGravatar barras2003-12-17
| | | | | | | reparation bug affichage des clauses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5108 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ suppression 250Gravatar herbelin2003-12-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5105 85f007b7-540e-0410-9357-904b9bb8a0f7
* modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesGravatar barras2003-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction bug: parentheses ne cassent plus les implicitesGravatar barras2003-12-08
| | | | | | | on met la notation ( _ ) qu'autour des entiers positifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5078 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace ↵Gravatar herbelin2003-12-04
| | | | | | par un niveau ajoute dynamiquement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5068 85f007b7-540e-0410-9357-904b9bb8a0f7
* Symetrisation parsing/printing 'abstract'Gravatar herbelin2003-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5066 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle tactique EExistsGravatar clrenard2003-12-01
| | | | | | | Changement des exports pour tactic EXTEND : with_bindings devient bindings qui prend plus le with, il faut le mettre à la main dans la règle. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5052 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout ne_stringGravatar herbelin2003-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5002 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection contre les notations videsGravatar herbelin2003-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4999 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traduction de tactic:constrarg en constr:constr pour les arguments de Tactic ↵Gravatar herbelin2003-11-26
| | | | | | Notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4996 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-02 18:14:17 +0000