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
2008-04-29
Suppression de la partie ML de la contrib correctness. Les fichiers
herbelin
2007-12-06
Plus de combinateurs sont passés de Util à Option. Le module Options
aspiwack
2007-08-27
Suppression des type_app et body_of_type qui alourdissent inutilement le code
herbelin
2006-04-28
Standardisation du nom des méthodes de Evd
herbelin
2006-01-11
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2005-02-06
Nettoyage et documentation de Library
herbelin
2004-07-16
Nouvelle en-tête
herbelin
2003-11-14
Correction chemin de Z
herbelin
2003-10-10
Affichage des buts par Pfedit pour utilisation par les tactiques
herbelin
2003-08-14
code mort
herbelin
2003-05-21
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-19
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-03-12
* Ajout du traducteur nouvelle syntaxe *
barras
2002-12-15
Evaluation paresseuse de l'affichage du debug
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-08-02
Modules dans COQ\!\!\!\!
coq
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