diff options
| author |  vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-12 09:45:02 +0000 |
|---|---|---|
| committer | vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-12 09:45:02 +0000 |
| commit | 9c8fdb79a0e43ae3d7bf7ed94c7dafad572fd61a (patch) | |
| tree | 1f37e5b4f5897c2af272b4c9a11fc0343138eb50 /toplevel/command.ml | |
| parent | 479313019612114e9c9fbb789af4bc7a48bb3cea (diff) | |
* 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
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index ffe4c26d5..210a79b08 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 |