aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernac.ml
Commit message (Expand)AuthorAge
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...Gravatar herbelin2007-02-24
* Cleaning backtracking code, optimized "Backtrack n x y" when n isGravatar courtieu2006-12-28
* Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms deGravatar herbelin2006-11-21
* Indentation + svnpropGravatar notin2006-09-12
* Réinitialisation de token_number à chaque compilation d'un nouveau fichier ...Gravatar notin2006-06-08
* Autres suppressions de composantes du traducteurGravatar herbelin2005-12-27
* 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
* Globalisation des Tactic NotationGravatar herbelin2005-05-15
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
* Abstraction vis à vis du type loc pour compatibilité ocaml 3.08Gravatar herbelin2004-07-16
* Nouvelle en-têteGravatar herbelin2004-07-16
* Correction bug 'Time Load foo'Gravatar herbelin2004-05-25
* pb facto des Fixpoint + erreur avec -dump-glob et LoadGravatar barras2004-04-17
* Ajout entree pour exporter les debuts et fins de compilation en mode -xmlGravatar herbelin2004-03-26
* modif des fixpoints pour que si on donne une notation au produit, les pts fix...Gravatar barras2004-03-05
* Localisation des erreurs d'internalisation des notations de tactiquesGravatar herbelin2004-02-12
* Protection table des locations lors de Load (pour coqdoc)Gravatar herbelin2004-01-22
* *** empty log message ***Gravatar barras2003-12-24
* Bug: faut brancher la sortie des tactiques sur stdout pendant traductionGravatar herbelin2003-11-18
* Mise en place traduction des tactiques apres evaluation pour permettre des ch...Gravatar herbelin2003-11-09
* bug traduction de auto.(simpl). en auto.simpl.Gravatar barras2003-10-20
* oups! ca compile maintenantGravatar barras2003-10-16
* translator avoids printing a . followed by a ( by inserting a spaceGravatar barras2003-10-16
* changement nouvelle syntaxe (pt fixes)Gravatar barras2003-10-10
* pr_vernac est paresseux; States.unfreeze seulement après que msgnl aitGravatar herbelin2003-10-03
* Traduction aussi si -translate et -load-vernac-sourceGravatar herbelin2003-09-24
* traducteur: affiche les commentaires a l'interieur des commandesGravatar barras2003-09-22
* Plutôt que de faire "Load" silencieusement, en profiter pour traduireGravatar herbelin2003-09-18
* Pour cacher le contenu de Load au traducteurGravatar herbelin2003-09-16
* Debranchement du traducteur pour Load !Gravatar herbelin2003-09-10
* Freeze mal placeGravatar herbelin2003-09-02
* Bug et amliorations diversesGravatar herbelin2003-08-12
* Ajout systématique de Proof dans la traductionGravatar herbelin2003-06-23
* Possibilité de syntaxe conjointement à la définition des inductifs et des ...Gravatar herbelin2003-05-21
* Affichage commentairesGravatar herbelin2003-05-13
* Factorisation des produits de même type; parenthèses autour des x:=c et n:=...Gravatar herbelin2003-04-29
* Bug fermeture de stdoutGravatar herbelin2003-04-29
* Formattage affichageGravatar herbelin2003-04-09
* Mécanisme plus simple et efficace pour traduire les implicitesGravatar herbelin2003-04-09
* Bugs synchronisation pour gestion traduction des implicitesGravatar herbelin2003-04-09
* Réorganisation de Impargs + mise en place d'une infrastructureGravatar herbelin2003-04-09
* *** empty log message ***Gravatar barras2003-03-12
* Recuperation des outputs de l'interpretation des commandes vernac et des erre...Gravatar desmettr2003-02-28
* Undo dans Coq IDEGravatar filliatr2003-02-11
* Ajout du traducteurGravatar desmettr2003-02-05
* deplacement du test 'il reste des preuves en cours'Gravatar filliatr2003-01-20
* Ajout options -v7 et -v8, et commandes V7only et V8onlyGravatar herbelin2002-12-10
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14