diff options
| author | msozeau | 2008-05-12 12:47:17 +0000 |
|---|---|---|
| committer | msozeau | 2008-05-12 12:47:17 +0000 |
| commit | 651a23b4b21045733d44a4bc944b6b56d449fe2e (patch) | |
| tree | 20cd8bed5dc125e7cebb38e4fa516a9209ef2bf9 /interp | |
| parent | 7248f6cccfcca2b0d59b244e8789590794aefc45 (diff) | |
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
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 2 |
1 files changed, 2 insertions, 0 deletions
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 = |