Non exhaustive match fixed.

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

diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml
index c668d1c9be33420a1b9222a8646c8c3408b7a436..74fa6d038ce9f73800a060ddbd81f92596fe8916 100644 (file)
--- 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