index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tactics
/
eauto.mli
Age
Commit message (
Expand
)
Author
2010-03-05
Fix [autounfold] to accept general [in] clauses.
msozeau
2009-10-28
Integrate a few improvements on typeclasses and Program from the equations br...
msozeau
2009-09-17
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-07-09
Use the proper unification flags in e_exact. This makes exact fail a bit
msozeau
2008-04-21
- Parameterize unification by two sets of transparent_state, one for open
msozeau
2008-03-08
correction d'un bug d'efficacite dans Function (+ ajout de eauto_with_bases)
jforest
2008-02-14
Backtrack changes on eauto, move specialized version of eauto in
msozeau
2008-02-09
Fix the clrewrite tactic, change Relations.v to work on relations in Prop
msozeau
2008-02-08
Change implementation of resolution for typeclasses to use a customized
msozeau
2008-02-06
Work-in-progress to make eauto accept a list of goals as input and
msozeau
2007-04-28
Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.
herbelin
2007-04-18
- Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771
herbelin
2007-04-16
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
2006-01-28
Ajout option 'using lemmas' à auto/trivial/eauto
herbelin
2006-01-24
Suppression de la dépendance en Map.fold de ocaml dont la sémantique a
herbelin
2005-11-17
A la demande de Julien Forest
letouzey
2004-07-16
Nouvelle en-tête
herbelin
2003-09-18
Interface Eauto
herbelin
