diff options
| author | Matthieu Sozeau | 2014-04-28 13:42:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:59:01 +0200 |
| commit | 6bcefa6a9f6fb70334b5c68e8d17aedec5ca7b13 (patch) | |
| tree | d7bddd4c3110e0482b7d4ee4c6fb9d29a6cb3f30 /plugins/funind/indfun_common.ml | |
| parent | 338be26cee38bb97cfbec7e1fd10b74906be8515 (diff) | |
Fix funind w.r.t. universes
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 5d9c226b7f..0d1e600ee6 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -229,7 +229,7 @@ type function_info = (* let function_table = ref ([] : function_db) *) -let from_function = Summary.ref Cmap.empty ~name:"functions_db_fn" +let from_function = Summary.ref Cmap_env.empty ~name:"functions_db_fn" let from_graph = Summary.ref Indmap.empty ~name:"functions_db_gr" (* @@ -254,7 +254,7 @@ let cache_Function (_,(finfos)) = *) let cache_Function (_,finfos) = - from_function := Cmap.add finfos.function_constant finfos !from_function; + from_function := Cmap_env.add finfos.function_constant finfos !from_function; from_graph := Indmap.add finfos.graph_ind finfos !from_graph @@ -348,7 +348,7 @@ let pr_info f_info = str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl () let pr_table tb = - let l = Cmap.fold (fun k v acc -> v::acc) tb [] in + let l = Cmap_env.fold (fun k v acc -> v::acc) tb [] in Pp.prlist_with_sep fnl pr_info l let in_Function : function_info -> Libobject.obj = @@ -372,7 +372,7 @@ let find_or_none id = let find_Function_infos f = - Cmap.find f !from_function + Cmap_env.find f !from_function let find_Function_of_graph ind = |