index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
eauto.mli
Commit message (
Expand
)
Author
Age
*
Use the proper unification flags in e_exact. This makes exact fail a bit
msozeau
2009-07-09
*
- Parameterize unification by two sets of transparent_state, one for open
msozeau
2008-04-21
*
correction d'un bug d'efficacite dans Function (+ ajout de eauto_with_bases)
jforest
2008-03-08
*
Backtrack changes on eauto, move specialized version of eauto in
msozeau
2008-02-14
*
Fix the clrewrite tactic, change Relations.v to work on relations in Prop
msozeau
2008-02-09
*
Change implementation of resolution for typeclasses to use a customized
msozeau
2008-02-08
*
Work-in-progress to make eauto accept a list of goals as input and
msozeau
2008-02-06
*
Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.
herbelin
2007-04-28
*
- Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771
herbelin
2007-04-18
*
Export de simplest_eapply, utilisé dans la contrib interface
notin
2007-04-16
*
Suite unification apply et eapply (l'un et l'autre profite maintenant
herbelin
2007-04-16
*
Ajout option 'using lemmas' à auto/trivial/eauto
herbelin
2006-01-28
*
Suppression de la dépendance en Map.fold de ocaml dont la sémantique a
herbelin
2006-01-24
*
A la demande de Julien Forest
letouzey
2005-11-17
*
Nouvelle en-tête
herbelin
2004-07-16
*
Interface Eauto
herbelin
2003-09-18