Bug fixed in pack_coercions_obj. The context of the metas in the metasenv of

the CurrentProof was not translated correctly.

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index 844260480134d42fd61acc3efbae44b755ccd2ef..37744982e5689e4f6a7c005660fdc8a080b09538 100644 (file)
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -1099,7 +1099,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                 CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt);
                assert false
             | Uncertain _ ->
-               prerr_endline ("#### Coercion not packed (Uncercatin case): " ^
+               prerr_endline ("#### Coercion not packed (Uncerctain case): " ^
                 CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt);
                assert false)
       | _ -> assert false) (* the composite coercion must exist *)
@@ -1467,7 +1467,7 @@ let typecheck metasenv uri obj ~localization_tbl =
 ;;
 
 (* sara' piu' veloce che raffinare da zero? mah.... *)
-let pack_coercion metasenv t =
+let pack_coercion metasenv ctx t =
  let module C = Cic in
  let rec merge_coercions ctx =
    let aux = (fun (u,t) -> u,merge_coercions ctx t) in
@@ -1531,7 +1531,7 @@ let pack_coercion metasenv t =
        let pl = List.map (merge_coercions ctx) pl in
        C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
    | C.Fix (fno, fl) ->
-       let ctx =
+       let ctx' =
          List.fold_left
            (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l) 
            ctx fl
@@ -1539,12 +1539,12 @@ let pack_coercion metasenv t =
        let fl = 
          List.map 
            (fun (name,idx,ty,bo) -> 
-             (name,idx,merge_coercions ctx ty,merge_coercions ctx bo)) 
+             (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo)) 
          fl
        in
        C.Fix (fno, fl)
    | C.CoFix (fno, fl) ->
-       let ctx =
+       let ctx' =
          List.fold_left
            (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l) 
            ctx fl
@@ -1552,12 +1552,12 @@ let pack_coercion metasenv t =
        let fl = 
          List.map 
            (fun (name,ty,bo) -> 
-             (name, merge_coercions ctx ty, merge_coercions ctx bo)) 
+             (name, merge_coercions ctx ty, merge_coercions ctx' bo)) 
          fl 
        in
        C.CoFix (fno, fl)
  in
- merge_coercions [] t
+  merge_coercions ctx t
 ;;
 
 let pack_coercion_obj obj =
@@ -1567,48 +1567,52 @@ let pack_coercion_obj obj =
       let body = 
         match body with 
         | None -> None 
-        | Some body -> Some (pack_coercion [] body) 
+        | Some body -> Some (pack_coercion [] [] body) 
       in
-      let ty = pack_coercion [] ty in
+      let ty = pack_coercion [] [] ty in
         C.Constant (id, body, ty, params, attrs)
   | C.Variable (name, body, ty, params, attrs) ->
       let body = 
         match body with 
         | None -> None 
-        | Some body -> Some (pack_coercion [] body) 
+        | Some body -> Some (pack_coercion [] [] body) 
       in
-      let ty = pack_coercion [] ty in
+      let ty = pack_coercion [] [] ty in
         C.Variable (name, body, ty, params, attrs)
   | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
       let conjectures = 
         List.map 
           (fun (i, ctx, ty) -> 
             let ctx = 
-              List.map 
-                (function 
-                | Some (name, C.Decl t) -> 
-                    Some (name, C.Decl (pack_coercion conjectures t))
-                | Some (name, C.Def (t,None)) -> 
-                    Some (name, C.Def (pack_coercion conjectures t, None))
-                | Some (name, C.Def (t,Some ty)) -> 
-                    Some (name, C.Def (pack_coercion conjectures t, 
-                                    Some (pack_coercion conjectures ty)))
-                | None -> None) 
-                ctx 
+              List.fold_right 
+                (fun item ctx ->
+                  let item' =
+                   match item with
+                      Some (name, C.Decl t) -> 
+                        Some (name, C.Decl (pack_coercion conjectures ctx t))
+                    | Some (name, C.Def (t,None)) -> 
+                        Some (name,C.Def (pack_coercion conjectures ctx t,None))
+                    | Some (name, C.Def (t,Some ty)) -> 
+                        Some (name, C.Def (pack_coercion conjectures ctx t, 
+                                       Some (pack_coercion conjectures ctx ty)))
+                    | None -> None
+                  in
+                   item'::ctx
+                ) ctx []
             in
-            ((i,ctx,pack_coercion conjectures ty))) 
-          conjectures
+             ((i,ctx,pack_coercion conjectures ctx ty))
+          ) conjectures
       in
-      let body = pack_coercion conjectures body in
-      let ty = pack_coercion conjectures ty in
+      let body = pack_coercion conjectures [] body in
+      let ty = pack_coercion conjectures [] ty in
       C.CurrentProof (name, conjectures, body, ty, params, attrs)
   | C.InductiveDefinition (indtys, params, leftno, attrs) ->
       let indtys = 
         List.map 
           (fun (name, ind, arity, cl) -> 
-            let arity = pack_coercion [] arity in
+            let arity = pack_coercion [] [] arity in
             let cl = 
-              List.map (fun (name, ty) -> (name,pack_coercion [] ty)) cl 
+              List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl 
             in
             (name, ind, arity, cl))
           indtys