From aaa11ef4a3958fb980f15f8104d22b9d5fea43a9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 12 Jan 2005 15:08:35 +0000 Subject: [PATCH] fixed clean_and_fill --- helm/matita/matitaInterpreter.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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; -- 2.39.2