X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.ml;h=fbcac945ae0a50e9d188e5ada89e2210003c8c65;hb=d5e420ba0286d6b6ccab7101bdd75a1442385e06;hp=f14e3d1269044d63e15eec3e931c8bc7ab9e1c1b;hpb=de9a83f286eee12117fb478ea2db18f7faebac9a;p=helm.git

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index f14e3d126..fbcac945a 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -103,7 +103,7 @@ let add_constant ~uri ?body ~ty ~ugraph ?(params = []) ?(attrs = []) status =
     let obj = Cic.Constant (name, body, ty, params, attrs) in
     let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
     CicEnvironment.add_type_checked_term uri (obj, ugraph);
-    MetadataDb.index_constant ~dbd ~uri ~body ~ty;
+    MetadataDb.index_obj ~dbd ~uri; (* must be in the env *)
     let new_stuff = save_object_to_disk status uri obj in  
     MatitaLog.message (sprintf "%s constant defined" suri);
     { status with objects = new_stuff @ status.objects }
@@ -126,7 +126,7 @@ let add_inductive_def
     let obj = Cic.InductiveDefinition (types, params, leftno, attrs) in
     let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
     CicEnvironment.put_inductive_definition uri (obj, ugraph);
-    MetadataDb.index_inductive_def ~dbd ~uri ~types:types;
+    MetadataDb.index_obj ~dbd ~uri; (* must be in the env *)
     let new_stuff = save_object_to_disk status uri obj in
     MatitaLog.message (sprintf "%s inductive type defined" suri);
     let status = { status with objects = new_stuff @ status.objects } in