From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 25 Nov 2005 17:40:38 +0000 (+0000)
Subject: Non exhaustive match fixed.
X-Git-Tag: make_still_working~8094
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=55ce3c06e925133b778f23cc188f7abeb6686ac0;p=helm.git

Non exhaustive match fixed.
---

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