aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/retroknowledge.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-03-03 14:20:42 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-03-03 15:26:51 +0100
commit96f8d358c7d3c9a08ff2006f42716bc64937dad2 (patch)
treec7a6503e6b39681aee60e556827614b5b3512778 /kernel/retroknowledge.ml
parent49a764bd81ac1b21130d54a1808ce95b9992a36d (diff)
Fixing pervasive equalities. In particular, I removed the code that deleted
duplicates in kernel side effects. They were chosen according to an equality that was quite irrelevant, and as expected this patch did not break the test-suite.
Diffstat (limited to 'kernel/retroknowledge.ml')
-rw-r--r--kernel/retroknowledge.ml10
1 files changed, 8 insertions, 2 deletions
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 4dc01f890..0c03e3299 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -100,8 +100,14 @@ type proactive = entry Proactive.t
a finite type describing the fields to the field of proactive retroknowledge
(and then to make as many functions as needed in environ.ml) *)
-module Reactive =
- Map.Make (struct type t = entry let compare = compare end)
+module EntryOrd =
+struct
+ type t = entry
+ let make (e : entry) : constr = Obj.magic e (** WARNING: maybe to be updated. *)
+ let compare c1 c2 = Constr.compare (make c1) (make c2)
+end
+
+module Reactive = Map.Make (EntryOrd)
type reactive_end = {(*information required by the compiler of the VM *)
vm_compiling :