From: Enrico Tassi <enrico.tassi@inria.fr>
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;