From 60f396b240ce1e1a3622ecc512be62a168494efe Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 17 Aug 2018 12:40:51 +0200
Subject: Do not abstract over the named variable in unsafe introduction
 tactic.

There is no point in doing that. The term being abstracted does not contain the
named variable y, as it is an evar of the form ?e{Var x_1, ... Var x_n, Rel 1}.
In practice it means that only the binding creation matters, the substitution
behaving as the identity, and ending up costing for nothing.
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2a8ebe08ca..15f955079d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -125,7 +125,7 @@ let unsafe_intro env store decl b =
     let ninst = mkRel 1 :: inst in
     let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in
     let (sigma, ev) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in
-    (sigma, mkNamedLambda_or_LetIn decl ev)
+    (sigma, mkLambda_or_LetIn (NamedDecl.to_rel_decl decl) ev)
   end
 
 let introduction id =
-- 
cgit v1.2.3