diff options
| author |  mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-04 17:09:57 +0000 |
|---|---|---|
| committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-04 17:09:57 +0000 |
| commit | 885673cbec549d24bd57b9e16bfb5375e426101c (patch) | |
| tree | c3693a4e70758d70e9706f7f98c54f6f1bfa0ab7 /toplevel/vernacentries.ml | |
| parent | cc92b9228f3463ce06ad457a47ef2a9b1f39a727 (diff) | |
Modification Require From
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3376 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 9b977b846..c911633e8 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -558,8 +558,8 @@ let vernac_solve_existential = instantiate_nth_evar_com (*****************************) (* Auxiliary file management *) -let vernac_require_from export spec id filename = - Library.require_library_from_file spec (Some id) filename export +let vernac_require_from export spec filename = + Library.require_library_from_file spec None filename export let vernac_add_loadpath isrec pdir ldiropt = let alias = match ldiropt with @@ -1077,7 +1077,7 @@ let interp c = match c with | VernacSolveExistential (n,c) -> vernac_solve_existential n c (* Auxiliary file and library management *) - | VernacRequireFrom (exp,spec,id,f) -> vernac_require_from exp spec id f + | VernacRequireFrom (exp,spec,f) -> vernac_require_from exp spec f | VernacAddLoadPath (isrec,s,alias) -> vernac_add_loadpath isrec s alias | VernacRemoveLoadPath s -> vernac_remove_loadpath s | VernacAddMLPath (isrec,s) -> vernac_add_ml_path isrec s |