diff options
| author | Emilio Jesus Gallego Arias | 2020-03-30 18:58:24 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-31 05:17:16 -0400 |
| commit | 7afd5e9fb7ba9e5fc41e41fd54eb90ee8cb13993 (patch) | |
| tree | 1d8ee10d5c7a8f38d79863ca4a99e5d83e612aee /tactics/declare.mli | |
| parent | 0eadf776ba78dcfdcab842f38f5de871ed337376 (diff) | |
[proof] Improve comment and argument name.
As suggested by Gaëtan Gilbert.
Diffstat (limited to 'tactics/declare.mli')
| -rw-r--r-- | tactics/declare.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/declare.mli b/tactics/declare.mli index 6ea08d5b0e..615cffeae7 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -64,9 +64,9 @@ val definition_entry -> ?types:types -> ?univs:Entries.universes_entry -> ?eff:Evd.side_effects - -> ?univc:Univ.ContextSet.t - (** Universe-constraints attached to the body-only, used in vio / - vio-delayed opaque constants *) + -> ?univsbody:Univ.ContextSet.t + (** Universe-constraints attached to the body-only, used in + vio-delayed opaque constants and private poly universes *) -> constr -> Evd.side_effects proof_entry |