new more flexible compose, see matita/tests/compose.ma for a sample

[helm.git] / components / tactics / closeCoercionGraph.ml

diff --git a/components/tactics/closeCoercionGraph.ml b/components/tactics/closeCoercionGraph.ml
index 1f4c1d12b2182055ddf994bcfb9110475ac25e4e..3e64110987cef40500d3339e833f007204525f55 100644 (file)
--- 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
@@ -341,7 +351,9 @@ let close_coercion_graph src tgt uri baseuri =
                             (CoercDb.term_of_carr (CoercDb.Uri coer)) 
                             [] [] univ arity true
                         in
-                        assert (menv = []);
+                        if (menv = []) then
+                          prerr_endline 
+                            "MENV non empty after composing coercions";
                         build_obj t univ arity
                     | _ -> assert false 
                   ) (first_step, CicUniv.empty_ugraph) tl