From 0df0e9cc7d5db550136c1b4d31834cd8e1d8633e Mon Sep 17 00:00:00 2001
From: Paolo G. Giarrusso
Date: Mon, 25 May 2020 11:43:09 +0200
Subject: Fix #12406: fix Coq type error in dependent induction's Ltac

---
 theories/Program/Equality.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index b46ddaa32b..5862a08838 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -264,7 +264,7 @@ Class DependentEliminationPackage (A : Type) :=
 
 Ltac elim_tac tac p :=
   let ty := type of p in
-  let eliminator := eval simpl in (@elim (_ : DependentEliminationPackage ty)) in
+  let eliminator := eval simpl in (@elim _ (_ : DependentEliminationPackage ty)) in
     tac p eliminator.
 
 (** Specialization to do case analysis or induction.
-- 
cgit v1.2.3