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