diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-11 12:11:07 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-11 12:15:49 +0200 |
| commit | d4b3de96f524887013c0955bd5b90f0311f086e6 (patch) | |
| tree | ea87e31c9c4681911c9dede29de2d1b51a86deec /plugins/extraction/extraction.ml | |
| parent | d65496f09c4b68fa318783e53f9cd6d5c18e1eb7 (diff) | |
Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name
for the record binder of classes. This name is no longer generated
in the kernel but part of the declaration. Also cleanup the interface
to recognize primitive records based on an option type instead of a
dynamic check of the length of an array.
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index aa0232d19..ea2239673 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -215,7 +215,7 @@ let oib_equal o1 o2 = Array.equal Id.equal o1.mind_consnames o2.mind_consnames let eq_record x y = - Option.equal (fun (x, y) (x', y') -> Array.for_all2 eq_constant x x') x y + Option.equal (Option.equal (fun (_, x, y) (_, x', y') -> Array.for_all2 eq_constant x x')) x y let mib_equal m1 m2 = Array.equal oib_equal m1.mind_packets m1.mind_packets && |