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

[helm.git] / helm / ocaml / tactics / primitiveTactics.ml

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index e2fac6167bae90cd10c8e8c5df2b3a2eadaab434..8abb946c6686e27a64e9060b5089c5c35a69ce23 100644 (file)
--- 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")