diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/typeclasses.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 80207f652..34f8f07f9 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 |