diff options
Diffstat (limited to 'tactics/dhyp.ml')
| -rw-r--r-- | tactics/dhyp.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index e3dddacb0..0d4684e22 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -220,8 +220,7 @@ let (inDD,_) = cache_function = cache_dd; open_function = (fun i o -> if i=1 then cache_dd o); subst_function = subst_dd; - classify_function = classify_dd; - export_function = export_dd } + classify_function = classify_dd } let catch_all_sort_pattern = PMeta(Some (id_of_string "SORT")) let catch_all_type_pattern = PMeta(Some (id_of_string "TYPE")) |