1. bug fixed: in the last commit on NCicLibrary we forgot that

[helm.git] / matita / components / grafite_engine / grafiteEngine.ml

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 2acf844b0f21a39707d217d939636f8e1130d142..4ccf56653461877e85170d95e2ddb629f9fb1f4e 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -471,12 +471,13 @@ let compute_relevance uri =
 let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
   match cmd with
   | GrafiteAst.Include (loc, mode, fname) ->
-          let _root, baseuri, _fullpath, _rrelpath = 
+          let _root, baseuri, fullpath, _rrelpath = 
        Librarian.baseuri_of_script ~include_paths fname in
      let baseuri = NUri.uri_of_string baseuri in
      (* MATITA 1.0: keep WithoutPreferences? *)
      let alias_only = (mode = GrafiteAst.OnlyPreferences) in
-      GrafiteTypes.Serializer.require ~alias_only ~baseuri ~fname status
+      GrafiteTypes.Serializer.require
+       ~alias_only ~baseuri ~fname:fullpath status
   | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
   | GrafiteAst.NCoercion (loc, name, t, ty, source, target) ->
      let status, composites =