Skip to content

Commit

Permalink
Getting rid of hint base v62. Courtesy of TZ.
Browse files Browse the repository at this point in the history
  • Loading branch information
@herbelin
herbelin committed Oct 23, 2016
1 parent 1d5f90d commit 9d9fed6
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion inversionSL.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -395,7 +395,7 @@ Save lemma1_inv_systemSL.
Hint Resolve lemma1_inv_systemSL.

Goal forall (b : wsort) (M N : TS b), e_relSL _ M N -> e_invSL _ M N.
simple induction 1; intros; simpl in |- *; auto 11 with v62.
simple induction 1; intros; simpl in |- *; auto 11.
Save lemma1_invSL.
Hint Resolve lemma1_invSL.

Expand Down

0 comments on commit 9d9fed6

Please sign in to comment.