aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/tactic_debug.ml
Commit message (Expand)AuthorAge
* improve the amount of information given by the Ltac tactic debuggerGravatar bertot2006-08-28
* Protection mode Debug On contre Ctrl-DGravatar herbelin2006-05-05
* Messages de idtac et fail peuvent maintenant être des listes de string, int ...Gravatar herbelin2006-01-21
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Suppression de la dépendance en Tacmach pour pouvoir être appelé de top_pr...Gravatar herbelin2004-12-31
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* deplacement de clenv vers pretypingGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de...Gravatar herbelin2003-06-10
* Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...Gravatar herbelin2003-05-21
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* Ajout d'un message à FailTacGravatar herbelin2003-03-31
* Debugger plus informatifGravatar delahaye2003-02-13
* Plus du tout de backtracking dans "Match term"; vrai Exit dans débogueurGravatar herbelin2003-01-21
* Erreur sur precedent commitGravatar herbelin2003-01-19
* Restructuration interpréteur de tactique: plus d'évaluation partielle à la...Gravatar herbelin2003-01-19
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* compat ocaml 3.03Gravatar filliatr2001-12-13
* Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrRGravatar delahaye2001-10-23
* entetesGravatar filliatr2001-03-15
* Tactiques utilisateur + debuggerGravatar delahaye2000-10-30