diff options
| author | Anton Trunov | 2020-06-20 09:36:18 +0300 |
|---|---|---|
| committer | Anton Trunov | 2020-06-20 09:36:18 +0300 |
| commit | 43dba0d74b6cc39eea149c2908291e9108d21e71 (patch) | |
| tree | a0f7708f788e1de208954c47aa45801e67b3ceeb /theories/Program | |
| parent | 6cdccdeed882c072c84567aea085afdbb0401393 (diff) | |
| parent | 0df0e9cc7d5db550136c1b4d31834cd8e1d8633e (diff) | |
Merge PR #12407: Fix #12406: fix Coq type error in dependent induction's Ltac
Reviewed-by: anton-trunov
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. |