diff options
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 498b33b63..d2e95a74b 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') -> eq_constr x x') x y + 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 && |