index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
contrib
/
correctness
/
ptactic.ml
Age
Commit message (
Expand
)
Author
2002-06-19
ProgWf -> Zwf
filliatr
2002-06-03
Protection des tactiques contre l'utilisation sans le bon contexte de thories
herbelin
2002-05-29
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-04-02
- modifs de la condition de garde pour mieux tenir compte des raisonnements
barras
2002-02-08
affichages avec prterm_env et non prterm; deb_print pour vraiment ne rien fai...
filliatr
2001-12-17
le save de Correctness faisant assert false
barras
2001-12-13
compat ocaml 3.03
filliatr
2001-11-05
GROS COMMIT:
barras
2001-10-09
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-05-28
nettoyage
filliatr
2001-05-23
amelioration des messages d'erreurs vis a vis des evars
barras
2001-05-18
Modification afin de permettre plusieurs modifs successives d'une commande
clrenard
2001-04-23
expansion des constr purs
filliatr
2001-04-19
remplace Zarith par ZArith
mohring
2001-04-10
réparation Correctness; options Extraction (changement de syntaxe)
filliatr
2001-04-09
branchement extraction en standard (pas de Require)
filliatr
2001-04-05
mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4
filliatr
2001-04-04
renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...
filliatr
2001-03-30
branchement extraction (bytecode seulement)
filliatr
2001-03-29
mise en place de Correctness (ne compile pas encore)
filliatr