diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-03 03:23:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-03 03:23:05 +0100 |
| commit | 3ec4c04b4a2f497cd1b933dbf6b646b923ee6690 (patch) | |
| tree | e1a70997230748bd5d4fde997dd84b9f7b4f8587 /tactics/btermdn.ml | |
| parent | a13e33bc6b4cf637f0e3b94be15907d50cf48eea (diff) | |
Term dnets do no need to contain the afferent constr pattern in their nodes.
Diffstat (limited to 'tactics/btermdn.ml')
| -rw-r--r-- | tactics/btermdn.ml | 17 |
1 files changed, 4 insertions, 13 deletions
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index b93be6fc2..9492ae1a0 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -130,17 +130,12 @@ module Make = functor (Z : Map.OrderedType) -> struct - module X = struct - type t = constr_pattern*int - let compare = Pervasives.compare (** FIXME *) - end - module Y = struct type t = term_label let compare = compare_term_label end - module Dn = Dn.Make(X)(Y)(Z) + module Dn = Dn.Make(Y)(Z) type t = Dn.t @@ -165,16 +160,12 @@ struct let lookup = function | None -> (fun dn t -> - List.map - (fun ((c,_),v) -> (c,v)) - (Dn.lookup dn bounded_constr_val_discr (t,!dnet_depth))) + Dn.lookup dn bounded_constr_val_discr (t,!dnet_depth)) | Some st -> (fun dn t -> - List.map - (fun ((c,_),v) -> (c,v)) - (Dn.lookup dn (bounded_constr_val_discr_st st) (t,!dnet_depth))) + Dn.lookup dn (bounded_constr_val_discr_st st) (t,!dnet_depth)) - let app f dn = Dn.app (fun ((c,_),v) -> f(c,v)) dn + let app f dn = Dn.app f dn end |