From 9c8fdb79a0e43ae3d7bf7ed94c7dafad572fd61a Mon Sep 17 00:00:00 2001
From: vsiles
Date: Wed, 12 Mar 2008 09:45:02 +0000
Subject: * Catching a Not_found exception when trying to use Scheme Equality
 over inductives types using Parameters

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10658 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/command.ml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/toplevel/command.ml b/toplevel/command.ml
index ffe4c26d54..210a79b083 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -299,6 +299,7 @@ let declare_eq_scheme sp =
   let mib = Global.lookup_mind sp in
   let nb_ind = Array.length mib.mind_packets in
   let eq_array = Auto_ind_decl.make_eq_scheme sp in
+  try
     for i=0 to (nb_ind-1) do
     let cpack = Array.get mib.mind_packets i in
     let nam = id_of_string ((string_of_id cpack.mind_typename)^"_beq")
@@ -314,6 +315,9 @@ let declare_eq_scheme sp =
           Lib.add_anonymous_leaf (inScheme ((sp,i),mkConst cst));
           definition_message nam
     done
+  with Not_found -> 
+    error "Your type contains Parameter without a boolean equality"
+
 (* decidability of eq *)
 
 (* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k 
-- 
cgit v1.2.3