X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicElim.ml;fp=helm%2Focaml%2Fcic_proof_checking%2FcicElim.ml;h=74fa6d038ce9f73800a060ddbd81f92596fe8916;hb=55ce3c06e925133b778f23cc188f7abeb6686ac0;hp=c668d1c9be33420a1b9222a8646c8c3408b7a436;hpb=de331332663ed9e4673755268b35a0b0f717ff73;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml
index c668d1c9b..74fa6d038 100644
--- a/helm/ocaml/cic_proof_checking/cicElim.ml
+++ b/helm/ocaml/cic_proof_checking/cicElim.ml
@@ -268,7 +268,11 @@ let elim_of ~sort uri typeno =
       let paramsno = count_pi ty in (* number of (left or right) parameters *)
       let rightno = paramsno - leftno in
       let dependent = (strip_pi ty <> Cic.Sort Cic.Prop) in
-let head = match strip_pi ty with Cic.Sort s -> s in
+      let head =
+       match strip_pi ty with
+          Cic.Sort s -> s
+        | _ -> assert false
+      in
       let conslen = List.length constructors in
       let consno = ref (conslen + 1) in
       if