diff options
Diffstat (limited to 'pretyping/vernacexpr.ml')
| -rw-r--r-- | pretyping/vernacexpr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml index 3a49d6cf8..e15c3ad04 100644 --- a/pretyping/vernacexpr.ml +++ b/pretyping/vernacexpr.ml @@ -338,7 +338,7 @@ type nonrec vernac_expr = | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list - | VernacConstraint of glob_constraint list + | VernacConstraint of Glob_term.glob_constraint list (* Gallina extensions *) | VernacBeginSection of lident |