From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 10 Jun 2005 14:51:04 +0000 (+0000)
Subject: an assert failure changed to an exception and a bit of code cleanupt
X-Git-Tag: PRE_STORAGE~76
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6a5752ce7b5d3fc6fea133b49cf7fd7a9e03deb4;p=helm.git

an assert failure changed to an exception and a bit of code cleanupt
---

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index e2fac6167..8abb946c6 100644
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -26,9 +26,8 @@
 open ProofEngineHelpers
 open ProofEngineTypes
 
+exception TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple
 exception NotAnInductiveTypeToEliminate
-exception NotTheRightEliminatorShape
-exception NoHypothesesFound
 exception WrongUriToVariable of string
 
 (* lambda_abstract newmeta ty *)
@@ -527,6 +526,7 @@ let elim_tac ~term =
         | C.Sort C.Set  -> "_rec"
         | C.Sort C.CProp -> "_rec"
         | C.Sort (C.Type _)-> "_rect" 
+        | C.Meta (_,_) -> raise TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple
         | _ -> assert false
       in
        U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")