From 55ce3c06e925133b778f23cc188f7abeb6686ac0 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 25 Nov 2005 17:40:38 +0000
Subject: [PATCH] Non exhaustive match fixed.

---
 helm/ocaml/cic_proof_checking/cicElim.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

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
-- 
2.39.2