diff options
Diffstat (limited to 'plugins/funind/g_indfun.ml4')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 90af20b4c..9899b7b21 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -15,7 +15,8 @@ open Indfun_common open Indfun open Genarg open Stdarg -open Misctypes +open Tacarg +open Tactypes open Pcoq open Pcoq.Prim open Pcoq.Constr @@ -38,7 +39,9 @@ let pr_fun_ind_using_typed prc prlc _ opt_c = match opt_c with | None -> mt () | Some b -> - let (_, b) = b (Global.env ()) Evd.empty in + let env = Global.env () in + let evd = Evd.from_env env in + let (_, b) = b env evd in spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b) @@ -123,7 +126,7 @@ ARGUMENT EXTEND auto_using' END module Gram = Pcoq.Gram -module Vernac = Pcoq.Vernac_ +module Vernac = Pvernac.Vernac_ module Tactic = Pltac type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located |