X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicRefine.ml;h=b50667bb5546a745ac53420827f0cdbd1d300dc6;hb=0bc1d5f7eb6c9ba8603c59a4d671d4b186e48508;hp=9fb3548d6e4362d8a621b50939f55f85763b5b18;hpb=0f76dec7bd31a5914c27c38fb28bf2279a7cdbc1;p=helm.git

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index 9fb3548d6..b50667bb5 100644
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -1983,7 +1983,13 @@ let pack_coercion metasenv ctx t =
   merge_coercions ctx t
 ;;
 
-let pack_coercion_metasenv conjectures =
+let pack_coercion_metasenv conjectures = conjectures (*
+
+  TASSI: this code war written when coercions were a toy,
+         now packing coercions involves unification thus
+         the metasenv may change, and this pack coercion 
+         does not handle that.
+
   let module C = Cic in
   List.map 
     (fun (i, ctx, ty) -> 
@@ -2006,9 +2012,16 @@ let pack_coercion_metasenv conjectures =
        in
          ((i,ctx,pack_coercion conjectures ctx ty))
     ) conjectures
+    *)
 ;;
 
-let pack_coercion_obj obj =
+let pack_coercion_obj obj = obj (*
+
+  TASSI: this code war written when coercions were a toy,
+         now packing coercions involves unification thus
+         the metasenv may change, and this pack coercion 
+         does not handle that.
+
   let module C = Cic in
   match obj with
   | C.Constant (id, body, ty, params, attrs) -> 
@@ -2043,7 +2056,7 @@ let pack_coercion_obj obj =
             (name, ind, arity, cl))
           indtys
       in
-        C.InductiveDefinition (indtys, params, leftno, attrs)
+        C.InductiveDefinition (indtys, params, leftno, attrs) *)
 ;;