From b8bf1433f739c8befdf410ace0a0ff6e779a3339 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 4 Mar 2014 12:07:04 +0000 Subject: [PATCH] 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. --- matita/components/ng_refiner/nCicRefiner.ml | 1 + 1 file changed, 1 insertion(+) 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 ^ " |---> " ^ -- 2.39.2