From 2ac5353d24133cbca97a85617942d38aed0cc9a3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 25 May 2020 14:13:54 +0200
Subject: [declare] Remove mutual internals from Info.t structure.

We move the advanced proof initialization routine to Declare, and stop
exposing implementation internals in `Info.t` constructor.
---
 proofs/proof.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

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 ***)
-- 
cgit v1.2.3