]> matita.cs.unibo.it Git - helm.git/commitdiff
Unsharing removed since it is now used in Cic2acic.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 2 Sep 2005 13:01:37 +0000 (13:01 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 2 Sep 2005 13:01:37 +0000 (13:01 +0000)
helm/matita/matitaEngine.ml

index c2db06efaeee6b5a708caecd5735a9eace2a94d9..3c54f5a1b6730510751e2e96a88d331c38b163fc 100644 (file)
@@ -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