avoid fixing non-recursive terms

[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 bb01585d12ce603108b7948dcdad09082a57ac31..98bfef9d6f5c60a6b445e2c2feb400032e1955f6 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -802,6 +802,24 @@ 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 = 
+                match obj_kind with
+                | NCic.Fixpoint _ -> 
+                    NCicUntrusted.map_obj_kind (fix ()) obj_kind 
+                | _ -> obj_kind
+              in
               let obj = uri,height,[],[],obj_kind in
                NCicTypeChecker.typecheck_obj obj;
                let timestamp = NCicLibrary.add_obj uri obj in