diff options
Diffstat (limited to 'pretyping/miscops.ml')
| -rw-r--r-- | pretyping/miscops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index 0f0af5409..1b536bfda 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -29,7 +29,7 @@ let smartmap_cast_type f c = (** Equalities on [glob_sort] *) -let glob_sort_eq g1 g2 = match g1, g2 with +let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with | GProp, GProp -> true | GSet, GSet -> true | GType l1, GType l2 -> |