aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/recordops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/recordops.ml')
-rw-r--r--pretyping/recordops.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index f32eb0879..fdc7875d7 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -114,6 +114,8 @@ module MethodsDnet : Term_dnet.S
= Term_dnet.Make
(struct
type t = global_reference * Evd.evar * Evd.evar_map
+ (** ppedrot: FIXME: this is surely wrong, generic equality has nothing to
+ do w.r.t. evar maps. *)
let compare = Pervasives.compare
let subst = subst_id
let constr_of (_,ev,evm) = Evd.evar_concl (Evd.find evm ev)