aboutsummaryrefslogtreecommitdiff
path: root/contrib/correctness/ptactic.ml
AgeCommit message (Expand)Author
2002-06-19ProgWf -> Zwffilliatr
2002-06-03Protection des tactiques contre l'utilisation sans le bon contexte de thoriesherbelin
2002-05-29Nouveau 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 raisonnementsbarras
2002-02-08affichages avec prterm_env et non prterm; deb_print pour vraiment ne rien fai...filliatr
2001-12-17le save de Correctness faisant assert falsebarras
2001-12-13compat ocaml 3.03filliatr
2001-11-05GROS COMMIT:barras
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-05-28nettoyagefilliatr
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
2001-05-18Modification afin de permettre plusieurs modifs successives d'une commandeclrenard
2001-04-23expansion des constr pursfilliatr
2001-04-19remplace Zarith par ZArithmohring
2001-04-10réparation Correctness; options Extraction (changement de syntaxe)filliatr
2001-04-09branchement extraction en standard (pas de Require)filliatr
2001-04-05mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4filliatr
2001-04-04renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...filliatr
2001-03-30branchement extraction (bytecode seulement)filliatr
2001-03-29mise en place de Correctness (ne compile pas encore)filliatr