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(-)

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