avoid the use of argument-free instantiate

plclub · Jun 23, 2024 · 166f76a · 166f76a
1 parent badeeab
commit 166f76a
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/Fsub/Fsub_LetSum_Infrastructure.v b/Fsub/Fsub_LetSum_Infrastructure.v
@@ -604,7 +604,6 @@ Proof with eauto using subst_tt_type.
     intros;
     try rewrite subst_te_open_ee_var;
     try rewrite subst_te_open_te_var;
-    instantiate;
     eauto using subst_tt_type
   ].
 Qed.
@@ -625,7 +624,7 @@ Proof with auto.
     intros;
     try rewrite subst_ee_open_ee_var;
     try rewrite subst_ee_open_te_var;
-    instantiate;
+    idtac;
     auto
   ].
   Case "expr_var".