From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 tactics/leminv.ml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'tactics/leminv.ml')

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index a4cdc159..caf4c1ec 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -12,9 +12,9 @@ open Pp
 open CErrors
 open Util
 open Names
-open Term
 open Termops
 open Environ
+open Constr
 open EConstr
 open Vars
 open Namegen
@@ -232,9 +232,8 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let c = fill_holes pfterm in
   (* warning: side-effect on ownSign *)
   let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
-  let invProof = EConstr.Unsafe.to_constr invProof in
-  let p = Evarutil.nf_evars_universes sigma invProof in
-    p, sigma
+  let p = EConstr.to_constr sigma invProof in
+  p, sigma
 
 let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
   let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in
@@ -252,7 +251,7 @@ let add_inversion_lemma_exn ~poly na com comsort bool tac =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let sigma, c = Constrintern.interp_type_evars env sigma com in
-  let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env sigma comsort in
+  let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in
   try
     add_inversion_lemma ~poly na env sigma c sort bool tac
   with
-- 
cgit v1.2.3