Skip to content
Snippets Groups Projects
Commit fb211a17 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Document a Boolean in spec_patterns.

parent db7a2c58
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/proofmode/spec_patterns.v
+ 1
− 1
View file @ fb211a17
......@@ -15,7 +15,7 @@ Record spec_goal := SpecGoal {
Inductive spec_pat :=
| SForall : spec_pat
| SIdent : ident → spec_pat
| SPureGoal : bool → spec_pat
| SPureGoal (perform_done : bool) : spec_pat
| SGoal : spec_goal → spec_pat
| SAutoFrame : goal_kind → spec_pat.
......
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