diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-29 12:30:25 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-29 12:30:25 +0000 |
| commit | 73798a12d39b03e1823b93c1364a86d14e2eec0a (patch) | |
| tree | 1095b79d71bdacfcf2acc311b9e4a3aa98f64d4c /tactics/auto.mli | |
| parent | ea24960e35ee39f8ed719583886f7b56587a879c (diff) | |
Fix eauto still using delta when it shouldn't (should make CoRN compile
in reasonable time), add (unfinished) documentation on type classes.
Put some classes into Prop explicitely as singleton inductive types are
no longer in Prop by default even if all the arguments are (is that
really what we want? roconnor says no).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10868 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/auto.mli')
| -rw-r--r-- | tactics/auto.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/auto.mli b/tactics/auto.mli index 7853235be..5b151162c 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -141,6 +141,8 @@ val default_search_depth : int ref val auto_unif_flags : Unification.unify_flags (* Try unification with the precompiled clause, then use registered Apply *) +val unify_resolve_nodelta : (constr * clausenv) -> tactic + val unify_resolve : Unification.unify_flags -> (constr * clausenv) -> tactic (* [ConclPattern concl pat tacast]: |