X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicCoercion.ml;h=5e121ccfcb12c89595a051fe04758f1743203f9a;hb=c83721701dbbd44d3d547fdec6c4a5658322f424;hp=8a6e8a1c818f5f19a99ff816531a19eb9f3561fc;hpb=c3fc204cc02f1031b5d17fb0f2be1fc01e5c452f;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index 8a6e8a1c8..5e121ccfc 100644
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -134,3 +134,31 @@ let look_for_coercion status metasenv subst context infty expty =
           metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
       (CoercionSet.elements candidates)
 ;;
+
+(* CSC: very inefficient implementation!
+   Enrico, can we use a discrimination tree here? *)
+let match_coercion status ~metasenv ~subst ~context t =
+ let db =
+  DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) []
+ in
+  try
+   Some
+    (List.find
+      (fun (p,_,_) ->
+        try
+         let t =
+          match p,t with
+             NCic.Appl lp, NCic.Appl lt ->
+              (match fst (HExtlib.split_nth (List.length lp) lt) with
+                  [t] -> t
+                | l -> NCic.Appl l)
+           | _,NCic.Appl (he::_) -> he
+           | _,_ -> t
+         in
+          NCicReduction.alpha_eq metasenv subst context p t
+        with
+         Failure _ -> false (* raised by split_nth *)
+      ) db)
+  with
+   Not_found -> None
+;;