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
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