diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-18 15:47:53 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-18 15:47:53 +0000 |
| commit | 097fb66ba441ea2f3caf273cc9530b36938a3bd7 (patch) | |
| tree | 49fefa52c7ee4d854b83676cc53ad0bc495cf517 /tactics/autorewrite.ml | |
| parent | c14ccd1b8a3855d4eb369be311d4b36a355e46c1 (diff) | |
Removing unused code from Term_dnet.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16784 85f007b7-540e-0410-9357-904b9bb8a0f7
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 ()) ++ |