From 1cc5c0da0b5335c8773efd27e678178ef5e9c5f1 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 22 Mar 2013 16:45:35 +0000
Subject: Fix bug# 2994, 2971 about better error messages. Fix bug# 2956,
 porting fix from 8.4 branch

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

(limited to 'pretyping')

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 80207f6524..34f8f07f9d 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -382,7 +382,9 @@ let add_class cl =
   List.iter (fun (n, inst, body) ->
 	     match inst with
 	     | Some (Backward, pri) ->
-	       declare_instance pri false (ConstRef (Option.get body))
+	       (match body with
+	       | None -> Errors.error "Non-definable projection can not be declared as a subinstance"
+	       | Some b -> declare_instance pri false (ConstRef b))
 	     | _ -> ())
   cl.cl_projs
 
-- 
cgit v1.2.3