From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 16 Jun 2009 18:28:17 +0000 (+0000)
Subject: we fix recursive object reference with the correct height
X-Git-Tag: make_still_working~3863
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=990450048b555a5d850d3f43727c6d830713e3aa;p=helm.git

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 bb01585d1..1a88b0be1 100644
--- 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