diff options
Diffstat (limited to 'vernac/g_vernac.ml4')
| -rw-r--r-- | vernac/g_vernac.ml4 | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4 index 6c7df8cfa..0964d46ac 100644 --- a/vernac/g_vernac.ml4 +++ b/vernac/g_vernac.ml4 @@ -230,6 +230,7 @@ GEXTEND Gram ext = [ "+" -> true | -> false ]; "}" -> (l',ext) | ext = [ "}" -> true | "|}" -> false ] -> ([], ext) ] -> + let open UState in { univdecl_instance = l; univdecl_extensible_instance = ext; univdecl_constraints = fst cs; |