diff options
Diffstat (limited to 'tactics/dhyp.ml')
| -rw-r--r-- | tactics/dhyp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index 3d34a2d68..be4343b4f 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -206,7 +206,7 @@ let cache_dd (_,(_,na,dd)) = (str"The code which adds destructor hints broke;" ++ spc () ++ str"this is not supposed to happen") -let classify_dd (_,(local,_,_ as o)) = +let classify_dd (local,_,_ as o) = if local then Dispose else Substitute o let export_dd (local,_,_ as x) = if local then None else Some x |