Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh

1 files changed, 25 insertions, 3 deletions

diff --git a/library/summary.ml b/library/summary.ml
index 8e2abbf15b..19e7e5fd93 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -10,6 +10,8 @@ open Pp
 open Errors
 open Util
 
+module Dyn = Dyn.Make(struct end)
+
 type marshallable = [ `Yes | `No | `Shallow ]
 type 'a summary_declaration = {
   freeze_function : marshallable -> 'a;
@@ -20,8 +22,19 @@ let summaries = ref Int.Map.empty
 
 let mangle id = id ^ "-SUMMARY"
 
+let make_dyn (type a) (tag : a Dyn.tag) =
+  let infun x = Dyn.Dyn (tag, x) in
+  let outfun : (Dyn.t -> a) = fun dyn ->
+    let Dyn.Dyn (t, x) = dyn in
+    match Dyn.eq t tag with
+    | None -> assert false
+    | Some Refl -> x
+  in
+  (infun, outfun)
+
 let internal_declare_summary hash sumname sdecl =
-  let (infun, outfun) = Dyn.create (mangle sumname) in
+  let tag = Dyn.create (mangle sumname) in
+  let (infun, outfun) = make_dyn tag in
   let dyn_freeze b = infun (sdecl.freeze_function b)
   and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum)
   and dyn_init = sdecl.init_function in
@@ -164,8 +177,15 @@ let project_summary { summaries; ml_module } ?(complement=false) ids =
   List.filter (fun (id, _) -> List.mem id ids) summaries
 
 let pointer_equal l1 l2 =
+  let ptr_equal d1 d2 =
+    let Dyn.Dyn (t1, x1) = d1 in
+    let Dyn.Dyn (t2, x2) = d2 in
+    match Dyn.eq t1 t2 with
+    | None -> false
+    | Some Refl -> x1 == x2
+    in
   CList.for_all2eq
-    (fun (id1,v1) (id2,v2) -> id1 = id2 && Dyn.pointer_equal v1 v2) l1 l2
+    (fun (id1,v1) (id2,v2) -> id1 = id2 && ptr_equal v1 v2) l1 l2
 
 (** All-in-one reference declaration + registration *)
 
@@ -176,3 +196,5 @@ let ref ?(freeze=fun _ r -> r) ~name x =
       unfreeze_function = ((:=) r);
       init_function = (fun () -> r := x) };
   r
+
+let dump = Dyn.dump