diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrview.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 88a3e85211..ad0a31622c 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -194,9 +194,11 @@ let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal -> Pp.(str"interp-out: " ++ Printer.pr_econstr_env env sigma term)); tclUNIT (env,sigma,term) with e -> + (* XXX this is another catch all! *) + let e, info = Exninfo.capture e in Ssrprinters.ppdebug (lazy Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env glob)); - tclZERO e + tclZERO ~info e end (* Commits the term to the monad *) |