index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
vernacentries.ml
Commit message (
Expand
)
Author
Age
*
Amélioration message localisation constructions et modules
herbelin
2004-12-09
*
compatibility with POWERPC
gregoire
2004-11-22
*
New command "Print Rewrite HindDb dbname".
sacerdot
2004-11-17
*
Ajout 'Locate Module'
herbelin
2004-11-17
*
*** empty log message ***
gregoire
2004-11-12
*
Changement dans les boxed values .
gregoire
2004-11-12
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
restructuration des printers: proofs passe avant parsing
barras
2004-09-17
*
hiding the meta_map in evar_defs
barras
2004-09-15
*
"Print Setoids" command added.
sacerdot
2004-07-23
*
Nouvelle en-tête
herbelin
2004-07-16
*
updated printing of evar context (may loop ?)
corbinea
2004-06-30
*
search window
coq
2004-02-04
*
Bug focus
herbelin
2004-02-03
*
Ajout option raw_print (Set Printing All) pour desactiver toute fonctionnalit...
herbelin
2004-01-29
*
Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...
herbelin
2004-01-29
*
Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a...
herbelin
2004-01-13
*
meilleure presentation des commentaires du traducteur
barras
2004-01-02
*
Bug rattrapage erreur locate_reference
herbelin
2003-12-20
*
option -n de coq-tex
marche
2003-12-12
*
Monstrueuse inefficacite due a l'innocence du redacteur de la ligne vis a vis...
herbelin
2003-11-27
*
Traitement plus clair, notamment pour Locate, de quand quoter les composantes...
herbelin
2003-11-22
*
Ajout Print Implicit avec depliage du type
herbelin
2003-11-15
*
Check bavard meme en mode silencieux, car on l'a voulu
herbelin
2003-11-14
*
Prise en compte des alias syntaxiques vers des references dans divers lieux d...
herbelin
2003-11-12
*
Idtac peut prendre un argument à afficher
narboux
2003-11-12
*
Re-suppression de is_verbose dans Print, pour coqide
herbelin
2003-11-10
*
Suppression SearchNamed finalement redondant avec SearchAbout
herbelin
2003-11-10
*
Branchement de Show Script sur l'afficheur structure
herbelin
2003-11-05
*
Debranchement de Print si pas verbose (necessaire pour traducteur)
herbelin
2003-11-01
*
Ajout de Print Visibility
herbelin
2003-10-28
*
Independance de grammar.cmo vis a vis de Search; reorganisation VernacDefinition
herbelin
2003-10-23
*
Integration de SearchNamed dans SearchAbout
herbelin
2003-10-22
*
reorganisation des niveaux (ex: = est a 70)
barras
2003-10-22
*
Debranchement de l'affichage systematique des projections avec la notation po...
herbelin
2003-10-16
*
Petits bugs
herbelin
2003-10-13
*
Deplacement pr_subgoal and co vers Pfedit; Ajout SearchNamed
herbelin
2003-10-13
*
Renommage en v8 de PolyList en List et List en MonoList
herbelin
2003-10-10
*
Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...
herbelin
2003-10-08
*
Debranchement de l'affichage automatique de Proof par le traducteur (trop com...
herbelin
2003-10-07
*
Correction du bug 335 et Export/Require Export dans un module
coq
2003-10-07
*
Ajout 'Close Scope'.
herbelin
2003-09-30
*
Ajout 'About'
herbelin
2003-09-26
*
Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...
herbelin
2003-09-23
*
Anglais
herbelin
2003-09-22
*
Renommage Implicits -> Implicit
herbelin
2003-09-21
*
Ajout 'Print Scopes' et 'Bind Scope with classes'
herbelin
2003-09-12
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
Ajout option Local à Hint, Hints et HintDestruct
herbelin
2003-06-14
*
Déplacement de code dans command; MAJ DebugOn
herbelin
2003-06-10
[next]