From 5135153d6cd2f22a82dd7209f46c02ed3f7c78cb Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 27 Aug 2020 12:16:15 +0200
Subject: Derive Inversion does not allow leftover evars

Fix #12917
---
 plugins/ltac/leminv.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml
index 47df3ec34f..f42c1f73a3 100644
--- a/plugins/ltac/leminv.ml
+++ b/plugins/ltac/leminv.ml
@@ -245,7 +245,8 @@ let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
 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 ~program_mode:false env sigma com in
+  let c, uctx = Constrintern.interp_type env sigma com in
+  let sigma = Evd.from_ctx uctx in
   let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in
   add_inversion_lemma ~poly na env sigma c sort bool tac
 
-- 
cgit v1.2.3