From 37fbe7f08c34c834f5cadcd425c276fe6ec4b42c Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Mon, 7 Nov 2016 13:36:38 +0100
Subject: COMMENT: Proof_global.pstate.pid

---
 proofs/proof_global.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index e4cba6f07d..3ee6fd40ff 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -88,7 +88,7 @@ type proof_terminator = proof_ending -> unit
 type closed_proof = proof_object * proof_terminator
 
 type pstate = {
-  pid : Id.t;
+  pid : Id.t;  (* the name of the theorem whose proof is being constructed *)
   terminator : proof_terminator CEphemeron.key;
   endline_tactic : Genarg.glob_generic_argument option;
   section_vars : Context.Named.t option;
-- 
cgit v1.2.3