index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
tauto.ml4
Commit message (
Expand
)
Author
Age
*
Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR
delahaye
2001-10-23
*
Ajout du printer de tactiques + modif du Dynamic ocaml
delahaye
2001-09-30
*
Parsing
herbelin
2001-08-10
*
Modification Tauto pour qu'il puisse destructurer des hypotheses de la forme
courant
2001-08-08
*
Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...
herbelin
2001-06-25
*
Fix d'un bug de Tauto
delahaye
2001-06-15
*
Correction d'un bug du a un Intros trop violent
delahaye
2001-06-01
*
Ajout du cas True->A|-B
delahaye
2001-04-24
*
entetes
filliatr
2001-03-15
*
Ajout d'une heuristique pour les types dependants
delahaye
2001-02-05
*
Message d'erreur plus explicite pour Tauto
delahaye
2001-02-05
*
rétablissement nouveau Tauto
filliatr
2001-02-05
*
Résolution d'un bug de simplification
delahaye
2001-02-03
*
oubli de Closure.EvalConstRef
filliatr
2001-02-01
*
- coqc : option -image
filliatr
2001-02-01
*
Bug fixed: the case [ id : ?1 -> ?2 |- ?] was missing in tauto_main
sacerdot
2001-01-30
*
As an heuristic, now both in tauto and intuition we try to avoid the initial
sacerdot
2001-01-29
*
Elimination du '
delahaye
2000-11-28
*
Nouveau choix pour l'intros initial
delahaye
2000-11-24
*
On n'introduit que des produits non dependants
delahaye
2000-11-23
*
compilation des fichiers ml4 sans GNUseries
filliatr
2000-11-03
*
Remplacement de Tauto et Intuition
delahaye
2000-10-30