aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacentries.ml
Commit message (Expand)AuthorAge
* compatibility with POWERPCGravatar gregoire2004-11-22
* New command "Print Rewrite HindDb dbname".Gravatar sacerdot2004-11-17
* Ajout 'Locate Module'Gravatar herbelin2004-11-17
* *** empty log message ***Gravatar gregoire2004-11-12
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* "Print Setoids" command added.Gravatar sacerdot2004-07-23
* Nouvelle en-têteGravatar herbelin2004-07-16
* updated printing of evar context (may loop ?)Gravatar corbinea2004-06-30
* search windowGravatar coq2004-02-04
* Bug focusGravatar herbelin2004-02-03
* Ajout option raw_print (Set Printing All) pour desactiver toute fonctionnalit...Gravatar herbelin2004-01-29
* 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
* meilleure presentation des commentaires du traducteurGravatar barras2004-01-02
* Bug rattrapage erreur locate_referenceGravatar herbelin2003-12-20
* option -n de coq-texGravatar marche2003-12-12
* Monstrueuse inefficacite due a l'innocence du redacteur de la ligne vis a vis...Gravatar herbelin2003-11-27
* Traitement plus clair, notamment pour Locate, de quand quoter les composantes...Gravatar herbelin2003-11-22
* Ajout Print Implicit avec depliage du typeGravatar herbelin2003-11-15
* Check bavard meme en mode silencieux, car on l'a vouluGravatar herbelin2003-11-14
* Prise en compte des alias syntaxiques vers des references dans divers lieux d...Gravatar herbelin2003-11-12
* Idtac peut prendre un argument à afficherGravatar narboux2003-11-12
* Re-suppression de is_verbose dans Print, pour coqideGravatar herbelin2003-11-10
* Suppression SearchNamed finalement redondant avec SearchAboutGravatar herbelin2003-11-10
* Branchement de Show Script sur l'afficheur structureGravatar herbelin2003-11-05
* Debranchement de Print si pas verbose (necessaire pour traducteur)Gravatar herbelin2003-11-01
* 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
* Debranchement de l'affichage systematique des projections avec la notation po...Gravatar herbelin2003-10-16
* Petits bugsGravatar herbelin2003-10-13
* Deplacement pr_subgoal and co vers Pfedit; Ajout SearchNamedGravatar herbelin2003-10-13
* Renommage en v8 de PolyList en List et List en MonoListGravatar herbelin2003-10-10
* Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...Gravatar herbelin2003-10-08
* Debranchement de l'affichage automatique de Proof par le traducteur (trop com...Gravatar herbelin2003-10-07
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
* Ajout 'Close Scope'.Gravatar herbelin2003-09-30
* Ajout 'About'Gravatar herbelin2003-09-26
* Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...Gravatar herbelin2003-09-23
* AnglaisGravatar herbelin2003-09-22
* Renommage Implicits -> ImplicitGravatar herbelin2003-09-21
* Ajout 'Print Scopes' et 'Bind Scope with classes'Gravatar herbelin2003-09-12
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
* Ajout option Local à Hint, Hints et HintDestructGravatar herbelin2003-06-14
* Déplacement de code dans command; MAJ DebugOnGravatar herbelin2003-06-10
* Ajout V8NotationGravatar herbelin2003-05-22