From: Claudio Sacerdoti Coen Date: Fri, 2 Sep 2005 13:01:37 +0000 (+0000) Subject: Unsharing removed since it is now used in Cic2acic. X-Git-Tag: V_0_1_2_1~116 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4658fcc5315ff90510a0e6ff7790156092ec44ce;p=helm.git Unsharing removed since it is now used in Cic2acic. --- diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index c2db06efa..3c54f5a1b 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -451,8 +451,6 @@ let generate_projections uri fields status = try let ty, ugraph = CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in - let bo = Unshare.unshare bo in - let ty = Unshare.unshare ty in let attrs = [`Class `Projection; `Generated] in let obj = Cic.Constant (name,Some bo,ty,[],attrs) in MatitaSync.add_obj uri obj status