diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-27 15:52:05 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-27 15:52:05 +0000 |
| commit | 64ac193d372ef8428e85010a862ece55ac011192 (patch) | |
| tree | d64af209e0a97f652918f500c3dd6a0ba1431bb7 /tactics/btermdn.mli | |
| parent | 7b74581cd633d28c83589dff1adf060fcfe87e8a (diff) | |
Enhanced discrimination nets implementation, which can now work with
goals containing existentials and use transparency information on
constants (optionally). Only used by the typeclasses eauto engine for
now, but could be used for other hint bases easily (just switch a boolean).
Had to add a new "creation" hint to be able to set said boolean upon
creation of the typeclass_instances hint db.
Improve the proof-search algorithm for Morphism, up to 10 seconds
gained in e.g. Field_theory, Ring_polynom. Added a morphism
declaration for [compose].
One needs to declare more constants as being unfoldable using
the [Typeclasses unfold] command so that discrimination is done correctly, but
that amounts to only 6 declarations in the standard library.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11184 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/btermdn.mli')
| -rw-r--r-- | tactics/btermdn.mli | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index e0ba8ddca..86107641d 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -11,6 +11,7 @@ (*i*) open Term open Pattern +open Names (*i*) (* Discrimination nets with bounded depth. *) @@ -19,10 +20,10 @@ type 'a t val create : unit -> 'a t -val add : 'a t -> (constr_pattern * 'a) -> 'a t -val rmv : 'a t -> (constr_pattern * 'a) -> 'a t - -val lookup : 'a t -> constr -> (constr_pattern * 'a) list +val add : transparent_state option -> 'a t -> (constr_pattern * 'a) -> 'a t +val rmv : transparent_state option -> 'a t -> (constr_pattern * 'a) -> 'a t + +val lookup : transparent_state option -> 'a t -> constr -> (constr_pattern * 'a) list val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit val dnet_depth : int ref |