aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacexpr.ml
Commit message (Expand)AuthorAge
* Suppression code pour hints nommés à la V7 (voire à la V6...)Gravatar herbelin2006-01-28
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Simplifification de vernac_expr li l'abandon du traducteurGravatar herbelin2005-12-23
* - debugging og "Show Intros": no line breaking + fresh idsGravatar coq2005-11-08
* New command: "Print Ltac qualid" to print user defined tactics.Gravatar sacerdot2005-05-20
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...Gravatar herbelin2005-05-17
* Implementation of a new backtracking system, that allow to go backGravatar coq2005-04-20
* Renaming Print Canonical Structure into Print Canonical ProjectionsGravatar herbelin2005-02-18
* Ajout Print Canonical StructuresGravatar herbelin2005-02-12
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Ajout de la syntaxe du reset label: "BackTo n".Gravatar coq2005-01-14
* - Module/Declare Module syntax made more uniform:Gravatar sacerdot2005-01-06
* New command "Print Rewrite HindDb dbname".Gravatar sacerdot2004-11-17
* Ajout 'Locate Module'Gravatar herbelin2004-11-17
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* "Print Setoids" command added.Gravatar sacerdot2004-07-23
* Nouvelle en-têteGravatar herbelin2004-07-16
* Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...Gravatar herbelin2004-01-29
* Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a...Gravatar herbelin2004-01-13
* bugs avec Pose et AssertGravatar barras2004-01-09
* meilleure presentation des commentaires du traducteurGravatar barras2004-01-02
* Ajout Print Implicit avec depliage du typeGravatar herbelin2003-11-15
* Suppression SearchNamed finalement redondant avec SearchAboutGravatar herbelin2003-11-10
* Ajout de Print VisibilityGravatar herbelin2003-10-28
* Independance de grammar.cmo vis a vis de Search; reorganisation VernacDefinitionGravatar herbelin2003-10-23
* Integration de SearchNamed dans SearchAboutGravatar herbelin2003-10-22
* reorganisation des niveaux (ex: = est a 70)Gravatar barras2003-10-22
* Changement 'as notation' en 'where notation'Gravatar herbelin2003-10-14
* Ajout d'une fonction de recherche sur les composantes du nom des objetsGravatar herbelin2003-10-13
* Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...Gravatar herbelin2003-10-08
* Ajout 'Close Scope'.Gravatar herbelin2003-09-30
* Ajout 'About'Gravatar herbelin2003-09-26
* Utilisation de noms dans 'Implicit Arguments [...]'Gravatar herbelin2003-09-23
* parsingGravatar herbelin2003-09-19
* Ajout 'Print Scopes' et 'Bind Scope with classes'Gravatar herbelin2003-09-12
* Mise en place possibilité de définitions locales dans les paramètres des r...Gravatar herbelin2003-09-06
* Mise en place possibilité de définitions locales dans les paramètres des i...Gravatar herbelin2003-09-06
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
* Ajout option Local à Hint, Hints et HintDestructGravatar herbelin2003-06-14
* Ajout V8NotationGravatar herbelin2003-05-22
* Possibilité de syntaxe conjointement à la définition des inductifs et des ...Gravatar herbelin2003-05-21
* Prise en compte des syntaxes v8 dans Uninterpreted NotationGravatar herbelin2003-04-29
* Ajout "at next level" dans NotationGravatar herbelin2003-04-17
* Ajout option 'Local' à Infix et NotationGravatar herbelin2003-04-11
* Ajout option "Local" à "Open Scope"Gravatar herbelin2003-04-08
* Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)Gravatar herbelin2003-03-29
* code mortGravatar herbelin2003-03-13
* *** empty log message ***Gravatar barras2003-03-12
* Ajout du traducteurGravatar desmettr2003-02-05