commented out pack coercion, since the code is not meaningfull.

it was conceived when coercions were toys, now it is much more complicated

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 9fb3548d6e4362d8a621b50939f55f85763b5b18..b50667bb5546a745ac53420827f0cdbd1d300dc6 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/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) *)
 ;;