From bff82b0ee42229e87bad101341fc5789d8199153 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 19 Sep 2007 07:20:39 +0000 Subject: [PATCH] commented out pack coercion, since the code is not meaningfull. it was conceived when coercions were toys, now it is much more complicated --- components/cic_unification/cicRefine.ml | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) 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) *) ;; -- 2.39.2