From aaea20533a92787a4b445fca01d0d90a2b59cce1 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 7 Feb 2020 15:21:32 +0100 Subject: 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. --- plugins/funind/functional_principles_proofs.ml | 8 ++++---- plugins/funind/gen_principle.ml | 4 ++-- plugins/funind/glob_term_to_relation.ml | 6 ++---- plugins/funind/invfun.ml | 6 +++--- plugins/funind/recdef.ml | 6 +++--- 5 files changed, 14 insertions(+), 16 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 00f4be783d..ad1c70b7bf 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -475,7 +475,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = tclIDTAC in try - scan_type [] (Typing.unsafe_type_of env sigma (mkVar hyp_id)), [hyp_id] + scan_type [] (Typing.type_of_variable env hyp_id), [hyp_id] with TOREMOVE -> thin [hyp_id],[] @@ -525,7 +525,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = tclMAP (fun id -> Proofview.V82.of_tactic (introduction id)) dyn_infos.rec_hyps; observe_tac "after_introduction" (fun g' -> (* We get infos on the equations introduced*) - let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in + let new_term_value_eq = pf_get_hyp_typ g' heq_id in (* compute the new value of the body *) let new_term_value = match EConstr.kind (project g') new_term_value_eq with @@ -849,7 +849,7 @@ let generalize_non_dep hyp g = (* observe (str "rec id := " ++ Ppconstr.pr_id hyp); *) let hyps = [hyp] in let env = Global.env () in - let hyp_typ = pf_unsafe_type_of g (mkVar hyp) in + let hyp_typ = pf_get_hyp_typ g hyp in let to_revert,_ = let open Context.Named.Declaration in Environ.fold_named_context_reverse (fun (clear,keep) decl -> @@ -1351,7 +1351,7 @@ let backtrack_eqs_until_hrec hrec eqs : tactic = let rewrite = tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs ) in - let _,hrec_concl = decompose_prod (project gls) (pf_unsafe_type_of gls (mkVar hrec)) in + let _,hrec_concl = decompose_prod (project gls) (pf_get_hyp_typ gls hrec) in let f_app = Array.last (snd (destApp (project gls) hrec_concl)) in let f = (fst (destApp (project gls) f_app)) in let rec backtrack : tactic = diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 58efee1518..8def5c60ba 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -617,7 +617,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i let constructor_args g = List.fold_right (fun hid acc -> - let type_of_hid = pf_unsafe_type_of g (mkVar hid) in + let type_of_hid = pf_get_hyp_typ g hid in let sigma = project g in match EConstr.kind sigma type_of_hid with | Prod(_,_,t') -> @@ -953,7 +953,7 @@ let rec reflexivity_with_destruct_cases g = match sc with None -> tclIDTAC g | Some id -> - match EConstr.kind (project g) (pf_unsafe_type_of g (mkVar id)) with + match EConstr.kind (project g) (pf_get_hyp_typ g id) with | App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind -> if Equality.discriminable (pf_env g) (project g) t1 t2 then Proofview.V82.of_tactic (Equality.discrHyp id) g diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index e41b92d4dc..bf32f7af19 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -769,9 +769,7 @@ and build_entry_lc_from_case_term env sigma types funname make_discr patterns_to let env_with_pat_ids = add_pat_variables sigma pat typ new_env in List.fold_right (fun id acc -> - let typ_of_id = - Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id) - in + let typ_of_id = Typing.type_of_variable env_with_pat_ids id in let raw_typ_of_id = Detyping.detype Detyping.Now false Id.Set.empty env_with_pat_ids (Evd.from_env env) typ_of_id @@ -832,7 +830,7 @@ and build_entry_lc_from_case_term env sigma types funname make_discr patterns_to (fun id acc -> if Id.Set.mem id this_pat_ids then (Prod (Name id), - let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in + let typ_of_id = Typing.type_of_variable new_env id in let raw_typ_of_id = Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_of_id in 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 diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 66ed1961ba..93ed1510d0 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -370,7 +370,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = Proofview.V82.of_tactic (clear to_intros); h_intros to_intros; (fun g' -> - let ty_teq = pf_unsafe_type_of g' (mkVar heq) in + let ty_teq = pf_get_hyp_typ g' heq in let teq_lhs,teq_rhs = let _,args = try destApp (project g') ty_teq with DestKO -> assert false in args.(1),args.(2) @@ -487,13 +487,13 @@ let rec prove_lt hyple g = in let h = List.find (fun id -> - match decompose_app sigma (pf_unsafe_type_of g (mkVar id)) with + match decompose_app sigma (pf_get_hyp_typ g id) with | _, t::_ -> EConstr.eq_constr sigma t varx | _ -> false ) hyple in let y = - List.hd (List.tl (snd (decompose_app sigma (pf_unsafe_type_of g (mkVar h))))) in + List.hd (List.tl (snd (decompose_app sigma (pf_get_hyp_typ g h)))) in observe_tclTHENLIST (fun _ _ -> str "prove_lt1")[ Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|]))); observe_tac (fun _ _ -> str "prove_lt") (prove_lt hyple) -- cgit v1.2.3