diff options
| author | Gaëtan Gilbert | 2020-02-07 15:21:32 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-07 15:21:32 +0100 |
| commit | aaea20533a92787a4b445fca01d0d90a2b59cce1 (patch) | |
| tree | a5987b56a9488413f66d7fd38cb5902ea0b0f11f /plugins/funind/invfun.ml | |
| parent | 51c0b1414be9a46e221b13f652474db0194093fc (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.ml | 6 |
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 |
