aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/proof.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 175c487958..a183fa7797 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -120,7 +120,7 @@ type t =
; name : Names.Id.t
(** the name of the theorem whose proof is being constructed *)
; poly : bool
- (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *)
+ (** polymorphism *)
}
(*** General proof functions ***)