aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/dn.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/dn.ml b/tactics/dn.ml
index cc811735ae..55112ba798 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -29,7 +29,7 @@ type ('lbl,'pat,'inf) under_t = (('lbl * int) option,'pat * 'inf) Tlm.t
type ('lbl,'pat,'inf) t = {
tm : ('lbl,'pat,'inf) under_t;
- args :('lbl,'pat) dn_args }
+ args : ('lbl,'pat) dn_args }
let create dna = {tm = Tlm.create(); args = dna}
@@ -61,7 +61,7 @@ let lookup dnm dna' t =
List.fold_left
(fun l c -> List.flatten(List.map (lookrec c) l))
(tm_of tm (Some(lbl,List.length v))) v)
- in
+ in
List.flatten(List.map Tlm.xtract (lookrec t dnm.tm))
let upd dnm f = { args = dnm.args; tm = f dnm.args dnm.tm }