diff options
Diffstat (limited to 'plugins')
| -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 0ddc7c0065..cce6aff287 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -207,7 +207,7 @@ let oib_equal o1 o2 = | RegularArity {mind_user_arity=c1; mind_sort=s1}, RegularArity {mind_user_arity=c2; mind_sort=s2} -> eq_constr c1 c2 && Sorts.equal s1 s2 | TemplateArity p1, TemplateArity p2 -> - let eq o1 o2 = Option.equal Univ.Universe.equal o1 o2 in + let eq o1 o2 = Option.equal Univ.Level.equal o1 o2 in List.equal eq p1.template_param_levels p2.template_param_levels && Univ.Universe.equal p1.template_level p2.template_level | _, _ -> false |