From: Enrico Tassi 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