maxipatch for support of multiple DBs.

[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 3e64110987cef40500d3339e833f007204525f55..d9dc679b32c35c85cafd5b25b68c66f45df554e3 100644 (file)
--- a/helm/software/components/tactics/closeCoercionGraph.ml
+++ b/helm/software/components/tactics/closeCoercionGraph.ml
@@ -77,7 +77,6 @@ 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
@@ -106,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])
@@ -229,6 +228,12 @@ 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 
@@ -311,8 +316,8 @@ let number_if_already_defined buri name l =
     if List.exists (UriManager.eq uri) l then retry ()
     else
       try
-        let _  = Http_getter.resolve' ~writable:true uri in
-        if Http_getter.exists' uri then retry () else uri
+        let _  = Http_getter.resolve' ~local:true ~writable:true uri in
+        if Http_getter.exists' ~local:true uri then retry () else uri
       with 
       | Http_getter_types.Key_not_found _ -> uri
       | Http_getter_types.Unresolvable_URI _ -> assert false
@@ -352,8 +357,7 @@ let close_coercion_graph src tgt uri baseuri =
                             [] [] univ arity true
                         in
                         if (menv = []) then
-                          prerr_endline 
-                            "MENV non empty after composing coercions";
+                          HLog.warn "MENV non empty after composing coercions";
                         build_obj t univ arity
                     | _ -> assert false 
                   ) (first_step, CicUniv.empty_ugraph) tl