the refiner was not checking that the resulting type

[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..037c5c6e2ce6b80f23e4bbacfe2f0471162e1b8b 100644 (file)
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -98,10 +98,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 +125,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: " ^