diff options
| author | Emilio Jesus Gallego Arias | 2020-05-25 14:13:54 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-26 14:38:10 +0200 |
| commit | 2ac5353d24133cbca97a85617942d38aed0cc9a3 (patch) | |
| tree | f20d64ad3dba698c30ddfb2c53a6d64fcdd0eeab /proofs/proof.ml | |
| parent | 43d381ab20035f64ce2edea8639fcd9e1d0453bc (diff) | |
[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.
Diffstat (limited to 'proofs/proof.ml')
| -rw-r--r-- | proofs/proof.ml | 2 |
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 ***) |