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