diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-20 18:17:58 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-27 19:47:52 +0100 |
| commit | 9243166490e8c939bbf6aa0316e99025b25e6398 (patch) | |
| tree | 391e1d205ee7a378774228404e5a7c00416e2d97 /stm | |
| parent | 6f240e9b15f2b6f6622c811933c4f5ffdf78cceb (diff) | |
[vernac] Adjust `interp` to pass polymorphic in the attributes.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 0ee9ea084..ab44cc98b 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1023,7 +1023,7 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t | VernacShow ShowScript -> ShowScript.show_script (); st | expr -> stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr); - try Vernacentries.interp ?verbosely:(Some verbose) ?proof st (Loc.tag ?loc expr) + try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (Loc.tag ?loc expr) with e -> let e = CErrors.push e in Exninfo.iraise Hooks.(call_process_error_once e) |