From 5112af4fd5df24b7272e69affcbb88edf1474b82 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 14:30:08 +0100 Subject: unsafe_type_of -> get_type_of in cases It goes in an error message so should be fine. --- pretyping/cases.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index cbd04a76ad..29d6726262 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2164,7 +2164,7 @@ let constr_of_pat env sigma arsign pat avoid = let IndType (indf, _) = try find_rectype env sigma (lift (-(List.length realargs)) ty) with Not_found -> error_case_not_inductive env sigma - {uj_val = ty; uj_type = Typing.unsafe_type_of env sigma ty} + {uj_val = ty; uj_type = Retyping.get_type_of env sigma ty} in let (ind,u), params = dest_ind_family indf in let params = List.map EConstr.of_constr params in -- cgit v1.2.3 From e566f2591b08f5575ba46815182dfdba29cde4fb Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 14:30:45 +0100 Subject: unsafe_type_of -> type_of in Tacred.pattern_occs This function already returns the evar map so no problem. --- pretyping/tacred.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 10e8cf7e0f..f87c50b5e4 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1197,7 +1197,7 @@ let abstract_scheme env sigma (locc,a) (c, sigma) = let pattern_occs loccs_trm = begin fun env sigma c -> let abstr_trm, sigma = List.fold_right (abstract_scheme env sigma) loccs_trm (c,sigma) in try - let _ = Typing.unsafe_type_of env sigma abstr_trm in + let sigma, _ = Typing.type_of env sigma abstr_trm in (sigma, applist(abstr_trm, List.map snd loccs_trm)) with Type_errors.TypeError (env',t) -> raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t)))) -- cgit v1.2.3 From 44d70e3e7d1101018dee45008b949c91d337438f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 14:33:11 +0100 Subject: unsafe_type_of -> type_of in Unification.applyHead We already thread the evar map --- pretyping/unification.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'pretyping') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 6486435ca2..2157c4ef6a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1274,12 +1274,14 @@ let applyHead env evd n c = else match EConstr.kind evd (whd_all env evd cty) with | Prod (_,c1,c2) -> - let (evd',evar) = - Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 in - apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd' + let (evd,evar) = + Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 + in + apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd | _ -> user_err Pp.(str "Apply_Head_Then") in - apprec n c (Typing.unsafe_type_of env evd c) evd + let evd, t = Typing.type_of env evd c in + apprec n c t evd let is_mimick_head sigma ts f = match EConstr.kind sigma f with -- cgit v1.2.3 From 92ffe0fb9d9b0390f56d11ae4fa3871064a17c74 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 6 Feb 2020 14:33:47 +0100 Subject: unsafe_type_of -> type_of in Pretyping.pretype_ref We already thread the evar map --- pretyping/pretyping.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index bf61d44a10..cb0c4868b5 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -446,7 +446,7 @@ let pretype_ref ?loc sigma env ref us = Pretype_errors.error_var_not_found ?loc !!env sigma id) | ref -> let sigma, c = pretype_global ?loc univ_flexible env sigma ref us in - let ty = unsafe_type_of !!env sigma c in + let sigma, ty = type_of !!env sigma c in sigma, make_judge c ty let interp_sort ?loc evd : glob_sort -> _ = function -- cgit v1.2.3 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. --- pretyping/typing.ml | 3 +++ pretyping/typing.mli | 3 +++ 2 files changed, 6 insertions(+) (limited to 'pretyping') diff --git a/pretyping/typing.ml b/pretyping/typing.ml index a15134f58d..4582844b71 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -253,6 +253,9 @@ let judge_of_type u = let judge_of_relative env v = Environ.on_judgment EConstr.of_constr (judge_of_relative env v) +let type_of_variable env id = + EConstr.of_constr (type_of_variable env id) + let judge_of_variable env id = Environ.on_judgment EConstr.of_constr (judge_of_variable env id) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 1b07b2bb78..fd2dc7c2fc 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -30,6 +30,9 @@ val sort_of : env -> evar_map -> types -> evar_map * Sorts.t (** Typecheck a term has a given type (assuming the type is OK) *) val check : env -> evar_map -> constr -> types -> evar_map +(** Type of a variable. *) +val type_of_variable : env -> variable -> types + (** Returns the instantiated type of a metavariable *) val meta_type : evar_map -> metavariable -> types -- cgit v1.2.3