From 651a23b4b21045733d44a4bc944b6b56d449fe2e Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 12 May 2008 12:47:17 +0000
Subject: Fix "not an applied typeclass" error for legitimate classes applied
 to no parameters.

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

(limited to 'interp/implicit_quantifiers.ml')

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index f6bd4fae3e..bb5a4412c9 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -172,11 +172,13 @@ let compute_context_vars env l =
 let destClassApp cl =
   match cl with
     | CApp (loc, (None,CRef ref), l) -> loc, ref, List.map fst l
+    | CRef ref -> loc_of_reference ref, ref, []
     | _ -> raise Not_found
       
 let destClassAppExpl cl =
   match cl with
     | CApp (loc, (None,CRef ref), l) -> loc, ref, l
+    | CRef ref -> loc_of_reference ref, ref, []
     | _ -> raise Not_found
 
 let full_class_binders env l = 
-- 
cgit v1.2.3