aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/tactic_debug.mli
Commit message (Expand)AuthorAge
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Makes the Ltac debugger usable again.Gravatar aspiwack2013-11-02
* Cutting the dependency of Genarg in constr_expr, glob_constrGravatar ppedrot2013-06-21
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Noise for nothingGravatar pboutill2012-03-02
* Breakpoints in Ltac debugger: new command "r foo" to jump to the nextGravatar herbelin2012-01-20
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Opened the possibility to type Ltac patterns but it is not fully functional yetGravatar herbelin2009-12-24
* 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