The left parameters coming from the constructor types have been refined in a

[helm.git] / helm / software / components / ng_refiner / nCicCoercion.ml

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index d168ba5488d9ffa1ccf92311887ab05da4767cba..fd697265a2464e4c9255eb6f844fd796b2fe6bac 100644 (file)
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -31,6 +31,12 @@ type db = DB.t * DB.t
 
 let empty_db = DB.empty,DB.empty
 
+class type g_status =
+ object
+  inherit NCicUnifHint.g_status
+  method coerc_db: db
+ end
+
 class status =
  object
   inherit NCicUnifHint.status
@@ -38,21 +44,18 @@ class status =
   method coerc_db = db
   method set_coerc_db v = {< db = v >}
   method set_coercion_status
-  : 'status. < coerc_db : db; uhint_db: NCicUnifHint.db; .. > as 'status -> 
-          'self
-          = fun o -> {< db = o#coerc_db >}#set_unifhint_status o
+   : 'status. #g_status as 'status -> 'self
+   = fun o -> {< db = o#coerc_db >}#set_unifhint_status o
  end
 
 let index_coercion status name c src tgt arity arg =
   let db_src,db_tgt = status#coerc_db in
   let data = (name,c,arity,arg,src,tgt) in
-
   debug (lazy ("INDEX:" ^ 
     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ "  :=  " ^
     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c ^ " " ^ 
     string_of_int arg ^ " " ^ string_of_int arity));
-
   let db_src = DB.index db_src src data in
   let db_tgt = DB.index db_tgt tgt data in
   status#set_coerc_db (db_src, db_tgt)
@@ -98,10 +101,13 @@ let index_old_db odb (status : #status) =
 
 let look_for_coercion status metasenv subst context infty expty =
  let db_src,db_tgt = status#coerc_db in
-  match infty, expty with
+  match 
+    NCicUntrusted.apply_subst subst context infty, 
+    NCicUntrusted.apply_subst subst context expty 
+  with
   | (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)), 
     (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> [] 
-  | _ ->
+  | infty, expty ->
 
     debug (lazy ("LOOK FOR COERCIONS: " ^ 
       NCicPp.ppterm ~metasenv ~subst ~context infty ^ "  |===> " ^
@@ -122,6 +128,16 @@ let look_for_coercion status metasenv subst context infty expty =
           CoercionSet.union (DB.retrieve_unifiables db_tgt expty) set)
         CoercionSet.empty tgt_class
     in
+
+    debug (lazy ("CANDIDATES SRC: " ^ 
+      String.concat "," (List.map (fun (name,t,_,_,_,_) ->
+        name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t) 
+      (CoercionSet.elements set_src))));
+    debug (lazy ("CANDIDATES TGT: " ^ 
+      String.concat "," (List.map (fun (name,t,_,_,_,_) ->
+        name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t) 
+      (CoercionSet.elements set_tgt))));
+
     let candidates = CoercionSet.inter set_src set_tgt in
 
     debug (lazy ("CANDIDATES: " ^