diff options
| author | Paolo G. Giarrusso | 2020-05-25 11:43:09 +0200 |
|---|---|---|
| committer | Paolo G. Giarrusso | 2020-05-25 11:43:09 +0200 |
| commit | 0df0e9cc7d5db550136c1b4d31834cd8e1d8633e (patch) | |
| tree | de2c634016b88e409b0717062b8f3446d0c81396 /theories/Program | |
| parent | 16e0877c6e3ec6228875e10afb1ec17d640eb1e9 (diff) | |
Fix #12406: fix Coq type error in dependent induction's Ltac
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Equality.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |