diff options
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d47c12a7cb..6ea2eb579f 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -839,7 +839,9 @@ let rec get_args b t : Constrexpr.local_binder_expr list * | _ -> [],b,t -let make_graph env sigma (f_ref : GlobRef.t) = +let make_graph (f_ref : GlobRef.t) = + let env = Global.env() in + let sigma = Evd.from_env env in let c,c_body = match f_ref with | ConstRef c -> @@ -907,11 +909,4 @@ let make_graph env sigma (f_ref : GlobRef.t) = expr_list; pstate) -let make_graph ~ontop f_ref = - let pstate = Option.map Proof_global.get_current_pstate ontop in - let sigma, env = Option.cata Pfedit.get_current_context - (let e = Global.env () in Evd.from_env e, e) pstate in - Option.cata (fun ps -> Some (Proof_global.push ~ontop ps)) ontop - (make_graph env sigma f_ref) - let do_generate_principle = do_generate_principle [] warning_error true |