index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
/
tactic_debug.ml
Commit message (
Expand
)
Author
Age
*
improve the amount of information given by the Ltac tactic debugger
bertot
2006-08-28
*
Protection mode Debug On contre Ctrl-D
herbelin
2006-05-05
*
Messages de idtac et fail peuvent maintenant être des listes de string, int ...
herbelin
2006-01-21
*
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2006-01-11
*
Suppression de la dépendance en Tacmach pour pouvoir être appelé de top_pr...
herbelin
2004-12-31
*
restructuration des printers: proofs passe avant parsing
barras
2004-09-17
*
deplacement de clenv vers pretyping
barras
2004-09-03
*
Nouvelle en-tête
herbelin
2004-07-16
*
Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de...
herbelin
2003-06-10
*
Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...
herbelin
2003-05-21
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
Ajout d'un message à FailTac
herbelin
2003-03-31
*
Debugger plus informatif
delahaye
2003-02-13
*
Plus du tout de backtracking dans "Match term"; vrai Exit dans débogueur
herbelin
2003-01-21
*
Erreur sur precedent commit
herbelin
2003-01-19
*
Restructuration interpréteur de tactique: plus d'évaluation partielle à la...
herbelin
2003-01-19
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
compat ocaml 3.03
filliatr
2001-12-13
*
Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR
delahaye
2001-10-23
*
entetes
filliatr
2001-03-15
*
Tactiques utilisateur + debugger
delahaye
2000-10-30