From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 19 Sep 2007 07:20:39 +0000 (+0000)
Subject: commented out pack coercion, since the code is not meaningfull.
X-Git-Tag: 0.4.95@7852~156
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=bff82b0ee42229e87bad101341fc5789d8199153

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/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) *)
 ;;