Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
RefinedC
Commits
ebf59ae4
Commit
ebf59ae4
authored
Apr 02, 2021
by
Rodolphe Lepigre
Browse files
Fix typo in error message.
parent
079c2b54
Pipeline
#44654
passed with stage
in 31 minutes and 19 seconds
Changes
1
Pipelines
7
Show whitespace changes
Inline
Side-by-side
theories/typing/automation/proof_state.v
View file @
ebf59ae4
...
...
@@ -140,5 +140,5 @@ Ltac print_typesystem_goal fn block :=
print_goal
;
admit
.
Ltac
print_sidecondition_goal
fn
:
=
idtac
"Cannot solve sidecondition in function"
fn
"!"
;
idtac
"Cannot solve side
condition in function"
fn
"!"
;
print_goal
;
admit
.
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a 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