Skip to content
Snippets Groups Projects
Commit bf999b6b authored by Dan Frumin's avatar Dan Frumin
Browse files

fix compliation

parent 95d81b30
No related branches found
No related tags found
No related merge requests found
Pipeline #48654 failed
Hide whitespace changes
Inline Side-by-side
theories/experimental/helping/helping_stack.v
+ 1
− 1
View file @ bf999b6b
...@@ -188,7 +188,7 @@ Section offerReg_rules. ...@@ -188,7 +188,7 @@ Section offerReg_rules.
symmetry. apply agree_included. symmetry. apply agree_included.
by apply to_agree_included. by apply to_agree_included.
+ rewrite lookup_singleton_ne; eauto. + rewrite lookup_singleton_ne; eauto.
by rewrite left_id. } simpl. by case_match. }
by rewrite Hfoo. by rewrite Hfoo.
Qed. Qed.
......
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