Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Benoit Viguier
coq-verif-tweetnacl
Commits
a68e8f9d
Commit
a68e8f9d
authored
Oct 01, 2020
by
benoit
Browse files
flow
parent
054d33a2
Changes
1
Hide whitespace changes
Inline
Side-by-side
paper/conclusion.tex
View file @
a68e8f9d
...
...
@@ -104,7 +104,7 @@ The tactics provided try to resolve those, and aim to simplify the workload of i
In an ideal world, the user does not need to know the lemmas applied under the hood and can just rely on those tactics.
Unfortunately, there were instances where those were not helping
% (\eg applying unnecessary substitutions, unfolding, exploding the size of our current goal; or simply failing),
at such moment,
it was
necessary to look into the VST code base and search for the right lemma.
at such moment,
making it
necessary to look into the VST code base and search for the right lemma.
Furthermore, the VST being an academic software, it is very hard to work with a tool
without being involved in the development loop. Additionally newer versions often broke
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment