diff options
Diffstat (limited to 'tactics/autorewrite.ml')
| -rw-r--r-- | tactics/autorewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index a4269b17c..c65c75f63 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -74,7 +74,7 @@ let find_rewrites bas = let find_matches bas pat = let base = find_base bas in let res = HintDN.search_pattern base pat in - List.map (fun ((_,rew), esubst, subst) -> rew) res + List.map snd res let print_rewrite_hintdb bas = (str "Database " ++ str bas ++ (Pp.cut ()) ++ |