index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
/
correctness
/
psyntax.ml4
Commit message (
Expand
)
Author
Age
*
Parenthesage du terme pour accepter 'of' comme non ident
herbelin
2003-12-24
*
'of' restait par erreur mot-cle dans psyntax.ml4 en v8
herbelin
2003-12-23
*
Remplacement de l'indicateur de date "@" par 'at'
herbelin
2003-11-26
*
Prise en compte renommages
herbelin
2003-11-19
*
traduction des noms de correctness
herbelin
2003-10-30
*
Traducteur de correctness
herbelin
2003-08-14
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
Ajout notation c.(f) en v8 pour les projections de Record
herbelin
2003-06-10
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
Court-circuit de g_zsyntax
herbelin
2002-11-28
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
retablissement de Correctness (pas encore teste' cependant)
filliatr
2002-09-18
*
Factorisation de 'Show Programs' au premier niveau de Vernac_.command
herbelin
2002-06-03
*
Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.v
herbelin
2002-05-29
*
code mort dans tactinterp; plus de Debug On/Off dans Correctness
filliatr
2002-02-21
*
Zinv -> Zopp
filliatr
2002-01-21
*
compat ocaml 3.03
filliatr
2001-12-13
*
nouvel algo de conversion plus uniforme
barras
2001-11-29
*
Fusion de declare/add_constant, declare/add_parameter et add_discharged_constant
herbelin
2001-11-20
*
GROS COMMIT:
barras
2001-11-05
*
Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR
delahaye
2001-10-23
*
Parsing
herbelin
2001-08-10
*
correction d'un bug de Correctness (pour Y Bertot)
filliatr
2001-06-27
*
nettoyage
filliatr
2001-05-28
*
documentation automatique de la bibliothèque standard
filliatr
2001-04-11
*
réparation Correctness; options Extraction (changement de syntaxe)
filliatr
2001-04-10
*
mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4
filliatr
2001-04-05
*
psyntax.ml4 sous CVS
filliatr
2001-04-03