Skip to content

Commit

Permalink
Merge pull request #125 from SkySkimmer/rename-update-env
Browse files Browse the repository at this point in the history
  • Loading branch information
jwiegley authored Jul 24, 2023
2 parents c7bde8d + fbce036 commit 7d8ba56
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion Lib/NETList.v
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ Inductive netlist {A : Type} (B : A → A → Type) : A → A → Type :=
Derive Signature NoConfusion NoConfusionHom Subterm for netlist.

Arguments tfin {A B i j} x.
Arguments tadd {A B i} j {k} x xs.
Arguments tadd {A B i} j {k} _ _.

Notation "x :::: xs" := (tadd _ x xs) (at level 60, right associativity).

Expand Down
2 changes: 1 addition & 1 deletion Lib/TList.v
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ Next Obligation.
Defined.

Arguments tnil {A B i}.
Arguments tcons {A B i} j {k} x xs.
Arguments tcons {A B i} j {k} _ _.

Notation "x ::: xs" := (tcons _ x xs) (at level 60, right associativity).

Expand Down

0 comments on commit 7d8ba56

Please sign in to comment.