diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-22 14:39:07 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-22 14:39:07 +0000 |
| commit | c9917c210da30521673e843b626359f4a1051e74 (patch) | |
| tree | f45a15f42956159752d6192ec7980081383330f9 /interp/reserve.ml | |
| parent | 14fdc212d664df129e2f718ea8b8eb87927a8ee8 (diff) | |
code simplifications concerning Summary
- Most of the time, the table registered via Summary.declare_summary
is just a single reference. A new function Summary.ref now allows
to both declare this ref and register it to summary in one shot.
- Clarifications concerning the role of [init_function].
For statically registered tables that don't need a special initializer,
just do nothing there (see the new Summary.nop function).
Beware: now that Summary exports a function named "ref", any code that
do an "open Summary" will probably fail to compile.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16441 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/reserve.ml')
| -rw-r--r-- | interp/reserve.ml | 15 |
1 files changed, 2 insertions, 13 deletions
diff --git a/interp/reserve.ml b/interp/reserve.ml index 30953007e..0efcafcd2 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -22,8 +22,8 @@ type key = | RefKey of global_reference | Oth -let reserve_table = ref Id.Map.empty -let reserve_revtable = ref Gmapl.empty +let reserve_table = Summary.ref Id.Map.empty ~name:"reserved-type" +let reserve_revtable = Summary.ref Gmapl.empty ~name:"reserved-type-rev" let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args) @@ -41,17 +41,6 @@ let in_reserved : Id.t * notation_constr -> obj = declare_object {(default_object "RESERVED-TYPE") with cache_function = cache_reserved_type } -let freeze_reserved () = (!reserve_table,!reserve_revtable) -let unfreeze_reserved (r,rr) = reserve_table := r; reserve_revtable := rr -let init_reserved () = - reserve_table := Id.Map.empty; reserve_revtable := Gmapl.empty - -let _ = - Summary.declare_summary "reserved-type" - { Summary.freeze_function = freeze_reserved; - Summary.unfreeze_function = unfreeze_reserved; - Summary.init_function = init_reserved } - let declare_reserved_type_binding (loc,id) t = if not (Id.equal id (root_of_id id)) then user_err_loc(loc,"declare_reserved_type", |