- pretty printer made robust in face of list_nth

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

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 97af8a06f7e0ab0d54b8652e11231fc259d0689d..4ab7412d832c60f4e0c0c0aab339e5ef9f2a652e 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -758,7 +758,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
              else
               let obj =
 prerr_endline "CSC: here we should fix the height!!!";
-               uri,height,[],[],NTacStatus.apply_subst_obj subst obj
+               uri,height,[],[],
+                NCicUntrusted.map_obj_kind (NCicUntrusted.apply_subst subst) obj
               in
                NCicLibrary.add_obj uri obj;
                {status with 
@@ -784,7 +785,8 @@ prerr_endline "CSC: here we should fix the height!!!";
           (* CSC: cut&paste code from NQed *)
           let obj =
 prerr_endline "CSC: here we should fix the height!!!";
-           uri,height,[],[],NTacStatus.apply_subst_obj nsubst nobj
+           uri,height,[],[],
+            NCicUntrusted.map_obj_kind (NCicUntrusted.apply_subst nsubst) nobj
           in
            NCicLibrary.add_obj uri obj;
            {status with