From c822b3de7f2a443cd920195fe94be1e7ceda3dbb Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 15:31:44 +0100
Subject: unsafe_type_of -> type_of in Tactics.intro_or_and_pattern

---
 tactics/tactics.ml | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3a4a2dc814..e859055d4a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2312,16 +2312,19 @@ let intro_decomp_eq ?loc l thin tac id =
 let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id =
   Proofview.Goal.enter begin fun gl ->
   let c = mkVar id in
-  let t = Tacmach.New.pf_unsafe_type_of gl c in
-  let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
+  let sigma, t = Typing.type_of env sigma c in
+  let (ind,t) = reduce_to_quantified_ind env sigma t in
   let branchsigns = compute_constructor_signatures ~rec_flag:false ind in
   let nv_with_let = Array.map List.length branchsigns in
   let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in
   let ll = get_and_check_or_and_pattern ?loc ll branchsigns in
-  Tacticals.New.tclTHENLASTn
-    (Tacticals.New.tclTHEN (simplest_ecase c) (clear [id]))
-    (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l)
-       nv_with_let ll)
+  Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+    (Tacticals.New.tclTHENLASTn
+       (Tacticals.New.tclTHEN (simplest_ecase c) (clear [id]))
+       (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l)
+          nv_with_let ll))
   end
 
 let rewrite_hyp_then assert_style with_evars thin l2r id tac =
-- 
cgit v1.2.3