X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=3aabdf1d4a2b915fa66b17901e217a75d20097ec;hb=3a430d712f9d87185e9271b7b0c5188c5f311e4b;hp=af8e1d87a1f31c62dded9015374d1786258bd117;hpb=f7da48c844105a52a705872dfa0d4104de010c82;p=helm.git

diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml
index af8e1d87a..3aabdf1d4 100644
--- a/matita/components/ng_refiner/nCicRefiner.ml
+++ b/matita/components/ng_refiner/nCicRefiner.ml
@@ -934,6 +934,7 @@ and try_coercions status
            | x::_ -> x 
            | _ -> assert false))
     | `XTProd -> C.Prod ("_",C.Implicit `Type,C.Implicit `Type)
+    | `XTInd -> assert false(*CSC: was not handled, OCaml 4.0 complains. ??? *)
   in
   pp(lazy("try_coercion " ^ 
     status#ppterm ~metasenv ~subst ~context infty ^ " |---> " ^