diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-16 15:01:07 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-16 15:01:07 +0000 |
| commit | 7ea13f14b30b74d644458464e3cd56d45b303f69 (patch) | |
| tree | ec1ed9462d111e397f8627ce453e0344cf42dd62 | |
| parent | e16cd2776ab7c779657bd73c58e0f77385c9e16f (diff) | |
bug : import -> export dans Require
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@260 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 280274788..765f3e9f6 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 _ = |