From b6144bc31b665cee95b3d443e05363e42feae386 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 20 Oct 2006 14:35:22 +0000
Subject: [PATCH] New function pack_coercion_metasenv, used in auto after
 try_candidates to clean up the metasenv (othewise application could fail).

---
 .../components/cic_unification/cicRefine.ml   | 49 ++++++++++---------
 .../components/cic_unification/cicRefine.mli  |  1 +
 2 files changed, 27 insertions(+), 23 deletions(-)

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 0a6510b44..dee8ba5f3 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1809,6 +1809,31 @@ let pack_coercion metasenv ctx t =
   merge_coercions ctx t
 ;;
 
+let pack_coercion_metasenv conjectures =
+  let module C = Cic in
+  List.map 
+    (fun (i, ctx, ty) -> 
+       let 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 ctx ty))
+    ) conjectures
+;;
+
 let pack_coercion_obj obj =
   let module C = Cic in
   match obj with
@@ -1829,29 +1854,7 @@ let pack_coercion_obj obj =
       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.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 ctx ty))
-          ) conjectures
-      in
+      let conjectures = pack_coercion_metasenv conjectures in
       let body = pack_coercion conjectures [] body in
       let ty = pack_coercion conjectures [] ty in
       C.CurrentProof (name, conjectures, body, ty, params, attrs)
diff --git a/helm/software/components/cic_unification/cicRefine.mli b/helm/software/components/cic_unification/cicRefine.mli
index be1069e71..30b264455 100644
--- a/helm/software/components/cic_unification/cicRefine.mli
+++ b/helm/software/components/cic_unification/cicRefine.mli
@@ -48,3 +48,4 @@ val insert_coercions: bool ref (* initially true *)
 
 val pack_coercion_obj: Cic.obj -> Cic.obj
 
+val pack_coercion_metasenv: Cic.metasenv -> Cic.metasenv
-- 
2.39.2