diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-07-09 15:32:28 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-07-09 15:32:28 +0000 |
| commit | 84c6dc6677ddf527a51eed62adcf8ad5daa77ca1 (patch) | |
| tree | dc2517398ee4242e9656c7420a5eb5a3c101d82a /tactics/eauto.mli | |
| parent | 2a596b2f6df4d884aaec99a519044036a4a81596 (diff) | |
Use the proper unification flags in e_exact. This makes exact fail a bit
more often but respects the spec better. The changes in the stdlib are
reduced to adding a few explicit [unfold]s in FMapFacts (exact was doing
conversion with delta on open terms in that case).
Also fix a minor bug in typeclasses not seeing typeclass evars when
their type was a (defined) evar itself.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12238 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/eauto.mli')
| -rw-r--r-- | tactics/eauto.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/eauto.mli b/tactics/eauto.mli index 1c6f9920f..d2ac36fe8 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -25,7 +25,7 @@ val e_assumption : tactic val registered_e_assumption : tactic -val e_give_exact_constr : constr -> tactic +val e_give_exact : ?flags:Unification.unify_flags -> constr -> tactic val gen_eauto : bool -> bool * int -> constr list -> hint_db_name list option -> tactic |