diff options
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 280274788b..765f3e9f6e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1092,7 +1092,7 @@ let _ = else Some (specif="SPECIFICATION")) (string_of_id id) None) - (import="IMPORT") + (import="EXPORT") | _ -> bad_vernac_args "Require") let _ = @@ -1108,7 +1108,7 @@ let _ = else Some (specif="SPECIFICATION")) (string_of_id id) (Some filename)) - (import="IMPORT")) + (import="EXPORT")) | _ -> bad_vernac_args "RequireFrom") let _ = |