Skip to content
Snippets Groups Projects
Commit d63de7cb authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Alpha renaming.

parent 4b213366
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/typing/tests/init_prod.v
+ 2
− 2
View file @ d63de7cb
...@@ -4,7 +4,7 @@ From lrust.typing Require Import programs product product_split own uniq_bor ...@@ -4,7 +4,7 @@ From lrust.typing Require Import programs product product_split own uniq_bor
shr_bor int function lft_contexts uninit cont borrow. shr_bor int function lft_contexts uninit cont borrow.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Section rebor. Section init_prod.
Context `{typeG Σ}. Context `{typeG Σ}.
Definition init_prod : val := Definition init_prod : val :=
...@@ -29,4 +29,4 @@ Section rebor. ...@@ -29,4 +29,4 @@ Section rebor.
eapply type_delete; [solve_typing..|]. eapply type_delete; [solve_typing..|].
eapply (type_jump [_]); solve_typing. eapply (type_jump [_]); solve_typing.
Qed. Qed.
End rebor. End init_prod.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment