Skip to content

Commit

Permalink
Backport for 8.17: Instance visibility flags
Browse files Browse the repository at this point in the history
  • Loading branch information
JoJoDeveloping committed Nov 7, 2023
1 parent 0ed8af2 commit c1b3cef
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions theories/Tennenbaum/Formulas.v
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,8 @@ Proof.
- apply sat_single. setoid_rewrite eval_num. now setoid_rewrite inu_nat_id.
Qed.

Existing Instance PA_preds_signature.
Existing Instance PA_funcs_signature.
#[global] Existing Instance PA_preds_signature.
#[global] Existing Instance PA_funcs_signature.

Definition unary α := bounded 1 α.
Definition binary α := bounded 2 α.
Expand Down

0 comments on commit c1b3cef

Please sign in to comment.