aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2014-04-18 10:33:24 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2014-05-06 09:59:01 +0200
commit338be26cee38bb97cfbec7e1fd10b74906be8515 (patch)
tree346f45227e94eb8bd4a5120b15192d3dd214b6f6 /plugins
parentda88175778d6055d1ecf40c8f429cf855a4304cb (diff)
Fix a pervasive equality use.
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/extraction.ml7
1 files changed, 5 insertions, 2 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index d8f28150a..f9dfd1fa4 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -210,16 +210,19 @@ let oib_equal o1 o2 =
end &&
Array.equal Id.equal o1.mind_consnames o2.mind_consnames
+let eq_record x y =
+ Option.equal (fun (x, y) (x', y') -> eq_constr x x') x y
+
let mib_equal m1 m2 =
Array.equal oib_equal m1.mind_packets m1.mind_packets &&
- (m1.mind_record) = m2.mind_record && (*FIXME*)
+ eq_record m1.mind_record m2.mind_record &&
(m1.mind_finite : bool) == m2.mind_finite &&
Int.equal m1.mind_ntypes m2.mind_ntypes &&
List.equal eq_named_declaration m1.mind_hyps m2.mind_hyps &&
Int.equal m1.mind_nparams m2.mind_nparams &&
Int.equal m1.mind_nparams_rec m2.mind_nparams_rec &&
List.equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt &&
- Pervasives.(=) m1.mind_universes m2.mind_universes (** FIXME *)
+ (* Univ.UContext.eq *) m1.mind_universes == m2.mind_universes (** FIXME *)
(* m1.mind_universes = m2.mind_universes *)
(*S Extraction of a type. *)