...

[helm.git] / helm / software / components / cic_unification / coercGraph.ml

diff --git a/helm/software/components/cic_unification/coercGraph.ml b/helm/software/components/cic_unification/coercGraph.ml
index 637944e6b8401e4df87c38e793c40a740d68da65..e54b3a847dde2d9489cf142baaa09f7b8b79cb11 100644 (file)
--- a/helm/software/components/cic_unification/coercGraph.ml
+++ b/helm/software/components/cic_unification/coercGraph.ml
@@ -70,7 +70,7 @@ let saturate_coercion ul metasenv subst context =
 ;;
           
 (* searches a coercion fron src to tgt in the !coercions list *)
-let look_for_coercion' metasenv subst context src tgt =
+let look_for_coercion_carr metasenv subst context src tgt =
   let is_dead = function CoercDb.Dead -> true | _ -> false in
   let pp_l s l =
    match l with
@@ -108,10 +108,18 @@ let look_for_coercion' metasenv subst context src tgt =
      | ul -> SomeCoercion (saturate_coercion ul metasenv subst context))
 ;;
 
+let rec count_pi c s t =
+  match CicReduction.whd ~delta:false ~subst:s c t with
+  | Cic.Prod (_,_,t) -> 1 + count_pi c s t
+  | _ -> 0
+;;
+
 let look_for_coercion metasenv subst context src tgt = 
-  let src_uri = CoercDb.coerc_carr_of_term src 0 in
-  let tgt_uri = CoercDb.coerc_carr_of_term tgt 0 in
-  look_for_coercion' metasenv subst context src_uri tgt_uri
+  let src_arity = count_pi context subst src in
+  let tgt_arity = count_pi context subst tgt in
+  let src_carr = CoercDb.coerc_carr_of_term src src_arity in
+  let tgt_carr = CoercDb.coerc_carr_of_term tgt tgt_arity in
+  look_for_coercion_carr metasenv subst context src_carr tgt_carr
 
 let source_of t = 
   match CoercDb.is_a_coercion t with
@@ -251,7 +259,7 @@ let rec min acc = function
   | [] -> acc
 ;;
 
-let meets metasenv subst context left right =
+let meets metasenv subst context (grow_left,left) (grow_right,right) =
   let saturate metasenv uo =
     match uo with 
     | None -> metasenv, None
@@ -262,8 +270,10 @@ let meets metasenv subst context left right =
   in
   List.map 
     (fun (c,uo1,uo2) -> 
-      let metasenv, uo1 = saturate metasenv uo1 in
-      let metasenv, uo2 = saturate metasenv uo2 in
+      let metasenv, uo1 = 
+        if grow_left then saturate metasenv uo1 else metasenv, None in
+      let metasenv, uo2 = 
+        if grow_right then saturate metasenv uo2 else metasenv, None in
       c,metasenv, uo1, uo2)
     (min [] (intersect (grow left) (grow right)))
 ;;