X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FcloseCoercionGraph.ml;h=3e64110987cef40500d3339e833f007204525f55;hb=c2a02fcbcaaef7358acebcb27014db4a601ad026;hp=4f1d1b182159eb334710bff22b2caa8a57d1e139;hpb=614e3c3fb219e404e60810bfc04072351803b8e8;p=helm.git

diff --git a/components/tactics/closeCoercionGraph.ml b/components/tactics/closeCoercionGraph.ml
index 4f1d1b182..3e6411098 100644
--- a/components/tactics/closeCoercionGraph.ml
+++ b/components/tactics/closeCoercionGraph.ml
@@ -78,6 +78,7 @@ exception UnableToCompose
  * both living in the same context and metasenv *)
 let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
   let module RT = RefinementTool in
+  let original_metasenv = metasenv in 
   let c1_ty,univ = CicTypeChecker.type_of_aux' metasenv context c1 univ in
   let c2_ty,univ = CicTypeChecker.type_of_aux' metasenv context c2 univ in
   let rec mk_implicits = function
@@ -177,8 +178,7 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
     List.sort 
       (fun (i,ctx1,ty1) (j,ctx1,ty1) -> 
           try List.assoc i meta2no -  List.assoc j meta2no 
-          with Not_found -> 
-            assert false) 
+          with Not_found -> assert false) 
       body_metasenv
   in
   let namer l n = 
@@ -221,6 +221,7 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
       let subst = create_subst_from_metas_to_rels spline_len body_metasenv in
       debug_print (lazy("SUBST: "^CicMetaSubst.ppsubst body_metasenv subst));
       let term = CicMetaSubst.apply_subst subst term in
+      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
       debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term));
       let term, ty, metasenv, ugraph = 
         CicRefine.type_of_aux' metasenv context term ugraph
@@ -229,6 +230,15 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
         split_metasenv metasenv (spline_len + List.length context)
       in
       let term = purge_unused_lambdas lambdas_metasenv term in
+      let metasenv = 
+        List.filter 
+          (fun (i,_,_) -> 
+            List.for_all 
+              (fun (j,_,_) ->
+                i <> j || List.exists (fun (j,_,_) -> j=i) original_metasenv) 
+              lambdas_metasenv) 
+          metasenv 
+      in
       debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term));
       debug_print(lazy("MENV: "^CicMetaSubst.ppmetasenv [] metasenv));
       term, metasenv, ugraph