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

Fix a warning

parent 5d15373a
No related branches found
No related tags found
No related merge requests found
Pipeline #27368 passed
...@@ -39,7 +39,7 @@ Section semtypes. ...@@ -39,7 +39,7 @@ Section semtypes.
| TExists τ' => λne Δ, lrel_exists (λ τ, interp τ' (τ::Δ)) | TExists τ' => λne Δ, lrel_exists (λ τ, interp τ' (τ::Δ))
| Tref τ => λne Δ, lrel_ref (interp τ Δ) | Tref τ => λne Δ, lrel_ref (interp τ Δ)
end. end.
Solve Obligations with (intros I τ τ' n Δ Δ' HΔ' ??; solve_proper). Solve Obligations with (intros I τ τ' n Δ Δ' HΔ' ??; try solve_proper).
Next Obligation. Next Obligation.
intros I τ τ' n Δ Δ' HΔ' ??. intros I τ τ' n Δ Δ' HΔ' ??.
apply lrel_rec_ne=> X /=. apply lrel_rec_ne=> X /=.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment