Bug partially fixed: the branch of a case of type Prod can be not a Lambda.

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 1b159510063ce13dfddb3f7b60fc881c84dfcde7..5363c5e64f3294a7c06c43277826c33065207d8e 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -459,9 +459,17 @@ and get_new_safes p c rl safes n nn x =
          if b then 1::safes' else safes'
         in
          get_new_safes ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
-   | (C.MutInd _, e, []) -> (e,safes,n,nn,x)
+   | (C.Prod _, (C.MutConstruct _ as e), _)
+   | (C.Prod _, (C.Rel _ as e), _)
+   | (C.MutInd _, e, [])
    | (C.Appl _, e, []) -> (e,safes,n,nn,x)
-   | (_,_,_) -> raise (Impossible 7)
+   | (_,_,_) ->
+      (* CSC: If the next exception is raised, it just means that   *)
+      (* CSC: the proof-assistant allows to use very strange things *)
+      (* CSC: as a branch of a case whose type is a Prod. In        *)
+      (* CSC: particular, this means that a new (C.Prod, x,_) case  *)
+      (* CSC: must be considered in this match. (e.g. x = MutCase)  *)
+      raise (Impossible 7)
 
 and split_prods n te =
  let module C = Cic in