From 6a5752ce7b5d3fc6fea133b49cf7fd7a9e03deb4 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 10 Jun 2005 14:51:04 +0000
Subject: [PATCH] an assert failure changed to an exception and a bit of code
 cleanupt

---
 helm/ocaml/tactics/primitiveTactics.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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