From 990450048b555a5d850d3f43727c6d830713e3aa Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 16 Jun 2009 18:28:17 +0000
Subject: [PATCH] we fix recursive object reference with the correct height
just before adding it to the library
---
.../components/grafite_engine/grafiteEngine.ml | 13 +++++++++++++
1 file changed, 13 insertions(+)
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
--
2.39.5