diff options
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 955ad9a88..4b4b36865 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -23,13 +23,7 @@ open Nameops open Misctypes (*i*) -let generalizable_table = ref Id.Pred.empty - -let _ = - Summary.declare_summary "generalizable-ident" - { Summary.freeze_function = (fun () -> !generalizable_table); - Summary.unfreeze_function = (fun r -> generalizable_table := r); - Summary.init_function = (fun () -> generalizable_table := Id.Pred.empty) } +let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident" let declare_generalizable_ident table (loc,id) = if not (Id.equal id (root_of_id id)) then |