many changes:

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

diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml
index 1f4c1d12b2182055ddf994bcfb9110475ac25e4e..898946ad64f6d89e77c0b18900644c55b0b8462c 100644 (file)
--- a/helm/software/components/tactics/closeCoercionGraph.ml
+++ b/helm/software/components/tactics/closeCoercionGraph.ml
@@ -77,7 +77,7 @@ exception UnableToCompose
 (* generate_composite (c2 (c1 s)) in the universe graph univ
  * 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
@@ -105,7 +105,7 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
   in
   let compose c1 nc1 c2 nc2 =
     Cic.Lambda 
-      (Cic.Name "x", (Cic.Implicit None),
+      (Cic.Name "x", (Cic.Implicit (Some `Type)),
           (Cic.Appl (  CicSubstitution.lift 1 c2 :: mk_implicits nc2 @ 
             [ Cic.Appl (  CicSubstitution.lift 1 c1 :: mk_implicits nc1 @ 
              [if last_lam_with_inn_arg then Cic.Rel 1 else Cic.Implicit None])
@@ -177,8 +177,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 +220,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
@@ -228,7 +228,22 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
       let body_metasenv, lambdas_metasenv = 
         split_metasenv metasenv (spline_len + List.length context)
       in
+      let lambdas_metasenv = 
+        List.filter 
+          (fun (i,_,_) -> 
+            List.for_all (fun (j,_,_) -> i <> j) original_metasenv)
+          lambdas_metasenv
+      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 +356,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