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.

1 files changed, 1 insertions, 1 deletions

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 =