diff options
Diffstat (limited to 'tactics/dhyp.ml')
| -rw-r--r-- | tactics/dhyp.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index d73677617..92db61f07 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -200,11 +200,10 @@ type destructor_data_object = identifier * destructor_data let ((inDD : destructor_data_object->obj), (outDD : obj->destructor_data_object)) = - declare_object ("DESTRUCT-HYP-CONCL-DATA", - { load_function = (fun _ -> ()); + declare_object {(default_object "DESTRUCT-HYP-CONCL-DATA") with cache_function = cache_dd; - open_function = cache_dd; - export_function = export_dd }) + open_function = (fun i o -> if i=1 then cache_dd o); + export_function = export_dd } let add_destructor_hint na loc pat pri code = begin match loc, code with |