From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 4 Mar 2014 12:07:04 +0000 (+0000)
Subject: OCaml 4.0 detects a not handled case.
X-Git-Tag: make_still_working~961
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=b8bf1433f739c8befdf410ace0a0ff6e779a3339

OCaml 4.0 detects a not handled case.
I hope the assertion will never be reached, but I ignore why.
I think this is really a bug and code must be written there.
---

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 ^ " |---> " ^