index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
translate
/
ppvernacnew.ml
Commit message (
Expand
)
Author
Age
*
"Print Setoids" command added.
sacerdot
2004-07-23
*
Abstraction vis à vis du type loc pour compatibilité ocaml 3.08
herbelin
2004-07-16
*
Nouvelle en-tête
herbelin
2004-07-16
*
pb facto des Fixpoint + erreur avec -dump-glob et Load
barras
2004-04-17
*
code mort
herbelin
2004-03-24
*
Traduction ad hoc pour Hint Rewrite in using
herbelin
2004-03-18
*
Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...
herbelin
2004-03-17
*
Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...
herbelin
2004-03-17
*
Mise en place de motifs récursifs dans Notation; quelques simplifications au...
herbelin
2004-03-17
*
modif des fixpoints pour que si on donne une notation au produit, les pts fix...
barras
2004-03-05
*
Plus de noms d'entrees de grammaires qualifies dans 'Tactic Notation'
herbelin
2004-03-03
*
Keep structure information for Fixpoint declaration and Fix terms
bertot
2004-02-26
*
Bugs/insuffisances trouvees en traduisant MMode
herbelin
2004-02-19
*
Suppression de 'Print.' en v8
herbelin
2004-01-29
*
Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a...
herbelin
2004-01-13
*
bugs avec Pose et Assert
barras
2004-01-09
*
certains id n'etaient pas renommes pour eviter les conflits avec les mots-cles
barras
2004-01-05
*
meilleure presentation des commentaires du traducteur
barras
2004-01-02
*
*** empty log message ***
barras
2003-12-24
*
Hint Destruct mal affiche
barras
2003-11-27
*
Traduction de tactic:constrarg en constr:constr pour les arguments de Tactic ...
herbelin
2003-11-26
*
Traduction Print Proof
herbelin
2003-11-25
*
Bug affichage Hint Extern
herbelin
2003-11-17
*
Ajout Print Implicit avec depliage du type
herbelin
2003-11-15
*
moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...
barras
2003-11-13
*
Traduction Print Grammar
herbelin
2003-11-13
*
Mise en place systeme de renommage des noms de variables liees dans la biblio...
herbelin
2003-11-12
*
Idtac peut prendre un argument à afficher
narboux
2003-11-12
*
petits changements de syntaxe
barras
2003-11-12
*
Suppression SearchNamed finalement redondant avec SearchAbout
herbelin
2003-11-10
*
Modules obsoletes de ZArith en v8
herbelin
2003-11-05
*
Pour eviter des anomalies au lieu d'erreur en mode traducteur
herbelin
2003-11-04
*
Ajout de Print Visibility
herbelin
2003-10-28
*
Independance de grammar.cmo vis a vis de Search; reorganisation VernacDefinition
herbelin
2003-10-23
*
Deplacement du pr_reference du traducteur dans Ppconstrnew; integration de Se...
herbelin
2003-10-22
*
reorganisation des niveaux (ex: = est a 70)
barras
2003-10-22
*
Changement 'as notation' en 'where notation'; protection 'nat_scope'; afficha...
herbelin
2003-10-14
*
Ajout d'une fonction de recherche sur les composantes du nom des objets
herbelin
2003-10-13
*
mise a jour nouvelle syntaxe
barras
2003-10-11
*
changement nouvelle syntaxe (pt fixes)
barras
2003-10-10
*
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
*
Essai de traduction du contraire de 'tacledit bin/coqtop.byte' en 'tac...'
herbelin
2003-10-07
*
Debranchement de l'affichage automatique de Proof par le traducteur (trop com...
herbelin
2003-10-07
*
Pas de renommage des noms de section
herbelin
2003-10-02
*
Implantation de l'option 'format' des Notations
herbelin
2003-10-01
*
Ajout 'Close Scope'.
herbelin
2003-09-30
*
Ajout 'About'
herbelin
2003-09-26
*
Utilisation de noms dans 'Implicit Arguments [...]'
herbelin
2003-09-23
*
traducteur: affiche les commentaires a l'interieur des commandes
barras
2003-09-22
[next]