aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/invfun.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2020-02-07 15:21:32 +0100
committerGaëtan Gilbert2020-02-07 15:21:32 +0100
commitaaea20533a92787a4b445fca01d0d90a2b59cce1 (patch)
treea5987b56a9488413f66d7fd38cb5902ea0b0f11f /plugins/funind/invfun.ml
parent51c0b1414be9a46e221b13f652474db0194093fc (diff)
various unsafe_type_of -> type_of_variable in funind
This is the easy part of removing unsafe_type_of, as type_of_variable doesn't return (or even take as argument) an evar map.
Diffstat (limited to 'plugins/funind/invfun.ml')
-rw-r--r--plugins/funind/invfun.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d72319d078..332d058ce7 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -28,7 +28,7 @@ open Indfun_common
*)
let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl ->
let sigma = project gl in
- let typ = pf_unsafe_type_of gl (mkVar hid) in
+ let typ = pf_get_hyp_typ hid gl in
match EConstr.kind sigma typ with
| App(i,args) when isInd sigma i ->
let ((kn',num) as ind'),u = destInd sigma i in
@@ -77,7 +77,7 @@ let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl ->
let functional_inversion kn hid fconst f_correct = Proofview.Goal.enter (fun gl ->
let old_ids = List.fold_right Id.Set.add (pf_ids_of_hyps gl) Id.Set.empty in
let sigma = project gl in
- let type_of_h = pf_unsafe_type_of gl (mkVar hid) in
+ let type_of_h = pf_get_hyp_typ hid gl in
match EConstr.kind sigma type_of_h with
| App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) ->
let pre_tac,f_args,res =
@@ -128,7 +128,7 @@ let invfun qhyp f =
| None ->
let tac_action hid gl =
let sigma = project gl in
- let hyp_typ = pf_unsafe_type_of gl (mkVar hid) in
+ let hyp_typ = pf_get_hyp_typ hid gl in
match EConstr.kind sigma hyp_typ with
| App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) ->
begin