diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-04-18 10:33:24 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:59:01 +0200 |
| commit | 338be26cee38bb97cfbec7e1fd10b74906be8515 (patch) | |
| tree | 346f45227e94eb8bd4a5120b15192d3dd214b6f6 /plugins/extraction/extraction.ml | |
| parent | da88175778d6055d1ecf40c8f429cf855a4304cb (diff) | |
Fix a pervasive equality use.
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 7 |
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. *) |