aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/tactic_debug.mli
Commit message (Expand)AuthorAge
* Add possibility to match on defined hypotheses, using brackets toGravatar msozeau2008-06-16
* improve the amount of information given by the Ltac tactic debuggerGravatar bertot2006-08-28
* Messages de idtac et fail peuvent maintenant être des listes de string, int ...Gravatar herbelin2006-01-21
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* premiere reorganisation de l\'unificationGravatar 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
* 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
* Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrRGravatar delahaye2001-10-23
* entetesGravatar filliatr2001-03-15
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Tactiques utilisateur + debuggerGravatar delahaye2000-10-30