diff options
| author |  Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:16 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:16 +0200 |
| commit | 813d651c75cb954677a483b60d880600b421e011 (patch) | |
| tree | f917021e7e7083cf1ce84f9a560179603f0c7af6 /toplevel/classes.ml | |
| parent | 0c6687c12b628881d5660d57707f0e7ca9e521b7 (diff) | |
| parent | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff) | |
Merge tag 'upstream/8.4pl2dfsg' into experimental/master
Upstream version 8.4pl2dfsg
Diffstat (limited to 'toplevel/classes.ml')
| -rw-r--r-- | toplevel/classes.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 6914b8f0..de4d1ab1 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -37,7 +37,10 @@ let set_typeclass_transparency c local b = let _ = Typeclasses.register_add_instance_hint (fun inst local pri -> - let path = try Auto.PathHints [global_of_constr inst] with _ -> Auto.PathAny in + let path = + try Auto.PathHints [global_of_constr inst] + with e when Errors.noncritical e -> Auto.PathAny + in Flags.silently (fun () -> Auto.add_hints local [typeclasses_db] (Auto.HintsResolveEntry @@ -300,8 +303,10 @@ let context l = let fullctx = Evarutil.nf_rel_context_evar !evars fullctx in let ce t = Evarutil.check_evars env Evd.empty !evars t in List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx; - let ctx = try named_of_rel_context fullctx with _ -> - error "Anonymous variables not allowed in contexts." + let ctx = + try named_of_rel_context fullctx + with e when Errors.noncritical e -> + error "Anonymous variables not allowed in contexts." in let fn (id, _, t) = if Lib.is_modtype () && not (Lib.sections_are_opened ()) then |