index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
vernac.ml
Commit message (
Expand
)
Author
Age
*
Plus de combinateurs sont passés de Util à Option. Le module Options
aspiwack
2007-12-06
*
Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...
herbelin
2007-02-24
*
Cleaning backtracking code, optimized "Backtrack n x y" when n is
courtieu
2006-12-28
*
Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms de
herbelin
2006-11-21
*
Indentation + svnprop
notin
2006-09-12
*
Réinitialisation de token_number à chaque compilation d'un nouveau fichier ...
notin
2006-06-08
*
Autres suppressions de composantes du traducteur
herbelin
2005-12-27
*
Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...
herbelin
2005-12-26
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Globalisation des Tactic Notation
herbelin
2005-05-15
*
Nettoyage et documentation de Library
herbelin
2005-02-06
*
Abstraction vis à vis du type loc pour compatibilité ocaml 3.08
herbelin
2004-07-16
*
Nouvelle en-tête
herbelin
2004-07-16
*
Correction bug 'Time Load foo'
herbelin
2004-05-25
*
pb facto des Fixpoint + erreur avec -dump-glob et Load
barras
2004-04-17
*
Ajout entree pour exporter les debuts et fins de compilation en mode -xml
herbelin
2004-03-26
*
modif des fixpoints pour que si on donne une notation au produit, les pts fix...
barras
2004-03-05
*
Localisation des erreurs d'internalisation des notations de tactiques
herbelin
2004-02-12
*
Protection table des locations lors de Load (pour coqdoc)
herbelin
2004-01-22
*
*** empty log message ***
barras
2003-12-24
*
Bug: faut brancher la sortie des tactiques sur stdout pendant traduction
herbelin
2003-11-18
*
Mise en place traduction des tactiques apres evaluation pour permettre des ch...
herbelin
2003-11-09
*
bug traduction de auto.(simpl). en auto.simpl.
barras
2003-10-20
*
oups! ca compile maintenant
barras
2003-10-16
*
translator avoids printing a . followed by a ( by inserting a space
barras
2003-10-16
*
changement nouvelle syntaxe (pt fixes)
barras
2003-10-10
*
pr_vernac est paresseux; States.unfreeze seulement après que msgnl ait
herbelin
2003-10-03
*
Traduction aussi si -translate et -load-vernac-source
herbelin
2003-09-24
*
traducteur: affiche les commentaires a l'interieur des commandes
barras
2003-09-22
*
Plutôt que de faire "Load" silencieusement, en profiter pour traduire
herbelin
2003-09-18
*
Pour cacher le contenu de Load au traducteur
herbelin
2003-09-16
*
Debranchement du traducteur pour Load !
herbelin
2003-09-10
*
Freeze mal place
herbelin
2003-09-02
*
Bug et amliorations diverses
herbelin
2003-08-12
*
Ajout systématique de Proof dans la traduction
herbelin
2003-06-23
*
Possibilité de syntaxe conjointement à la définition des inductifs et des ...
herbelin
2003-05-21
*
Affichage commentaires
herbelin
2003-05-13
*
Factorisation des produits de même type; parenthèses autour des x:=c et n:=...
herbelin
2003-04-29
*
Bug fermeture de stdout
herbelin
2003-04-29
*
Formattage affichage
herbelin
2003-04-09
*
Mécanisme plus simple et efficace pour traduire les implicites
herbelin
2003-04-09
*
Bugs synchronisation pour gestion traduction des implicites
herbelin
2003-04-09
*
Réorganisation de Impargs + mise en place d'une infrastructure
herbelin
2003-04-09
*
*** empty log message ***
barras
2003-03-12
*
Recuperation des outputs de l'interpretation des commandes vernac et des erre...
desmettr
2003-02-28
*
Undo dans Coq IDE
filliatr
2003-02-11
*
Ajout du traducteur
desmettr
2003-02-05
*
deplacement du test 'il reste des preuves en cours'
filliatr
2003-01-20
*
Ajout options -v7 et -v8, et commandes V7only et V8only
herbelin
2002-12-10
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
[next]