From: Enrico Tassi Date: Wed, 12 Jan 2005 15:08:35 +0000 (+0000) Subject: fixed clean_and_fill X-Git-Tag: V_0_1_0~140 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aaa11ef4a3958fb980f15f8104d22b9d5fea43a9;p=helm.git fixed clean_and_fill --- diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index 4521ab21b..f99e11854 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -305,7 +305,7 @@ class commandState Cic.Constant ((UriManager.name_of_uri uri), (Some body_cic),type_cic,[]) in -(* let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in *) + let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in CicEnvironment.add_type_checked_term uri (obj, ugraph); MetadataDb.index_constant ~dbd ~owner:(Helm_registry.get "matita.owner") ~uri @@ -319,8 +319,8 @@ class commandState let ugraph = CicTypeChecker.typecheck_mutual_inductive_defs uri (indTypes, params, leftno) CicUniv.empty_ugraph - in -(* let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in *) + in + let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in CicEnvironment.put_inductive_definition uri (obj, ugraph); MetadataDb.index_inductive_def ~dbd ~owner:(Helm_registry.get "matita.owner") ~uri ~types:indTypes; @@ -439,7 +439,7 @@ class proofState let obj = Cic.Constant ((UriManager.name_of_uri uri), (Some bo),ty,[]) in -(* let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in *) + let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in CicEnvironment.add_type_checked_term uri (obj, ugraph); MetadataDb.index_constant ~dbd ~owner:(Helm_registry.get "matita.owner") ~uri ~body:(Some bo) ~ty;