we fix recursive object reference with the correct height

just before adding it to the library

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index bb01585d12ce603108b7948dcdad09082a57ac31..1a88b0be1121c770307ebc1e3eb4a9b5f7b9c588 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -802,6 +802,19 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
                NCicUntrusted.map_obj_kind 
                 (NCicUntrusted.apply_subst subst []) obj_kind in
               let height = NCicTypeChecker.height_of_obj_kind uri obj_kind in
+              (* fix the height inside the object *)
+              let rec fix () = function 
+                | NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri -> 
+                   NCic.Const (NReference.reference_of_spec u
+                    (match spec with
+                    | NReference.Def _ -> NReference.Def height
+                    | NReference.Fix (i,j,_) -> NReference.Fix(i,j,height)
+                    | NReference.CoFix _ -> NReference.CoFix height
+                    | NReference.Ind _ | NReference.Con _
+                    | NReference.Decl as s -> s))
+                | t -> NCicUtils.map (fun _ () -> ()) () fix t
+              in
+              let obj_kind = NCicUntrusted.map_obj_kind (fix ()) obj_kind in
               let obj = uri,height,[],[],obj_kind in
                NCicTypeChecker.typecheck_obj obj;
                let timestamp = NCicLibrary.add_obj uri obj in