From 338be26cee38bb97cfbec7e1fd10b74906be8515 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 18 Apr 2014 10:33:24 +0200 Subject: Fix a pervasive equality use. --- plugins/extraction/extraction.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'plugins/extraction/extraction.ml') 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. *) -- cgit v1.2.3