diff options
| author |  puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-29 14:30:00 +0000 |
|---|---|---|
| committer | puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-29 14:30:00 +0000 |
| commit | 77e4d3059e0b513e0d3ef1a077ef4542fb6e679d (patch) | |
| tree | 88220c273d68e79c0d63cd8d516251e34fc5caa4 /plugins/field | |
| parent | 0daf358a71aff4aded2b822fc18b7a8b49cdbd04 (diff) | |
Field: generic Gmap on constr replaced by Cmap
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14370 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/field')
| -rw-r--r-- | plugins/field/field.ml4 | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4 index 1cba563ea..8b6bb133a 100644 --- a/plugins/field/field.ml4 +++ b/plugins/field/field.ml4 @@ -37,18 +37,20 @@ let constr_of_opt a opt = | None -> mkApp (init_constant "None",[|ac3|]) | Some f -> mkApp (init_constant "Some",[|ac3;constr_of f|]) +module Cmap = Map.Make(struct type t = constr let compare = constr_ord end) + (* Table of theories *) -let th_tab = ref (Gmap.empty : (constr,constr) Gmap.t) +let th_tab = ref (Cmap.empty : constr Cmap.t) let lookup env typ = - try Gmap.find typ !th_tab + try Cmap.find typ !th_tab with Not_found -> errorlabstrm "field" (str "No field is declared for type" ++ spc() ++ Printer.pr_lconstr_env env typ) let _ = - let init () = th_tab := Gmap.empty in + let init () = th_tab := Cmap.empty in let freeze () = !th_tab in let unfreeze fs = th_tab := fs in Summary.declare_summary "field" @@ -57,7 +59,7 @@ let _ = Summary.init_function = init } let load_addfield _ = () -let cache_addfield (_,(typ,th)) = th_tab := Gmap.add typ th !th_tab +let cache_addfield (_,(typ,th)) = th_tab := Cmap.add typ th !th_tab let subst_addfield (subst,(typ,th as obj)) = let typ' = subst_mps subst typ in let th' = subst_mps subst th in |