From 83b0822a9f6d5e35e9bfb1595a3466d7f4e3b12f Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 6 May 2008 16:33:56 +0000
Subject: Better parsing of typeclasses, any constr is allowed for ! bindings
 so notations work and bug #1846 gets completely fixed.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10890 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/implicit_quantifiers.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'interp/implicit_quantifiers.ml')

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index cf37efc77a..f6bd4fae3e 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -185,7 +185,11 @@ let full_class_binders env l =
     List.fold_left (fun (l', avoid) (iid, bk, cl as x) -> 
       match bk with
 	  Implicit -> 
-	    let (loc, id, l) = destClassAppExpl cl in
+	    let (loc, id, l) = 
+	      try destClassAppExpl cl 
+	      with Not_found -> 
+		user_err_loc (constr_loc cl, "class_binders", str"Not an applied type class")
+	    in
 	    let gr = Nametab.global id in
 	      (try
 		  let c = class_info gr in
-- 
cgit v1.2.3