Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Fix Ltac2 bug in Dawn file

Browse Source
This commit is contained in:
Danila Fedorin 2021-11-27 23:13:08 -08:00
parent abdc8e5056
commit d72e64c7f9
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
code/dawn/Dawn.v
View File

@ -131,7 +131,7 @@ Ltac2 rec solve_basic () := Control.enter (fun _ =>
| [|- Sem_int ?vs1 apply ?vs2] => apply Sem_apply | [|- Sem_int ?vs1 apply ?vs2] => apply Sem_apply
| [|- Sem_expr ?vs1 (e_comp ?e1 ?e2) ?vs2] => eapply Sem_e_comp; solve_basic () | [|- Sem_expr ?vs1 (e_comp ?e1 ?e2) ?vs2] => eapply Sem_e_comp; solve_basic ()
| [|- Sem_expr ?vs1 (e_int ?e) ?vs2] => apply Sem_e_int; solve_basic () | [|- Sem_expr ?vs1 (e_int ?e) ?vs2] => apply Sem_e_int; solve_basic ()
| [|- Sem_e_quote ?vs1 (e_quote ?e) ?vs2] => apply Sem_quote | [|- Sem_expr ?vs1 (e_quote ?e) ?vs2] => apply Sem_e_quote
| [_ : _ |- _] => () | [_ : _ |- _] => ()
end). end).