From fb211a177abf758ac64fe9dfb42d02612f18e370 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 10 Jan 2019 13:59:49 +0100
Subject: [PATCH] Document a Boolean in spec_patterns.

---
 theories/proofmode/spec_patterns.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/proofmode/spec_patterns.v b/theories/proofmode/spec_patterns.v
index 2332ebac5..a2f10edb1 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/theories/proofmode/spec_patterns.v
@@ -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.
 
-- 
GitLab