index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
/
correctness
/
ptactic.ml
Commit message (
Expand
)
Author
Age
*
Standardisation du nom des méthodes de Evd
herbelin
2006-04-28
*
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2006-01-11
*
Nettoyage et documentation de Library
herbelin
2005-02-06
*
Nouvelle en-tête
herbelin
2004-07-16
*
Correction chemin de Z
herbelin
2003-11-14
*
Affichage des buts par Pfedit pour utilisation par les tactiques
herbelin
2003-10-10
*
code mort
herbelin
2003-08-14
*
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-21
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
* Ajout du traducteur nouvelle syntaxe *
barras
2003-03-12
*
Evaluation paresseuse de l'affichage du debug
herbelin
2002-12-15
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
retablissement de Correctness (pas encore teste' cependant)
filliatr
2002-09-18
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
ProgWf -> Zwf
filliatr
2002-06-19
*
Protection des tactiques contre l'utilisation sans le bon contexte de thories
herbelin
2002-06-03
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
- modifs de la condition de garde pour mieux tenir compte des raisonnements
barras
2002-04-02
*
affichages avec prterm_env et non prterm; deb_print pour vraiment ne rien fai...
filliatr
2002-02-08
*
le save de Correctness faisant assert false
barras
2001-12-17
*
compat ocaml 3.03
filliatr
2001-12-13
*
GROS COMMIT:
barras
2001-11-05
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
nettoyage
filliatr
2001-05-28
*
amelioration des messages d'erreurs vis a vis des evars
barras
2001-05-23
*
Modification afin de permettre plusieurs modifs successives d'une commande
clrenard
2001-05-18
*
expansion des constr purs
filliatr
2001-04-23
*
remplace Zarith par ZArith
mohring
2001-04-19
*
réparation Correctness; options Extraction (changement de syntaxe)
filliatr
2001-04-10
*
branchement extraction en standard (pas de Require)
filliatr
2001-04-09
*
mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4
filliatr
2001-04-05
*
renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...
filliatr
2001-04-04
*
branchement extraction (bytecode seulement)
filliatr
2001-03-30
*
mise en place de Correctness (ne compile pas encore)
filliatr
2001-03-29