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.5