diff options
| author | Emilio Jesus Gallego Arias | 2020-04-10 03:46:57 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-03 17:25:55 +0200 |
| commit | eab9f3bd104f154c128955ff344eb671d0e2ec93 (patch) | |
| tree | bea8faeeb4f6f71cd80143d72dd61ea628b06579 /vernac/declare.mli | |
| parent | d4081616fafe3e9fa02cef2e0102a03638f70fd6 (diff) | |
[funind] Remove use of low-level entries in scheme generation.
This is needed to make this low-level entry structures privates;
moreover, the code seems much clearer using the higher-level API.
Some more cleanup needs to be done but this is clearly a step forward
IMHO.
Diffstat (limited to 'vernac/declare.mli')
| -rw-r--r-- | vernac/declare.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/declare.mli b/vernac/declare.mli index e23e148ddc..a297f25868 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -249,7 +249,7 @@ val build_by_tactic -> poly:bool -> typ:EConstr.types -> unit Proofview.tactic - -> Constr.constr * Constr.types option * bool * UState.t + -> Constr.constr * Constr.types option * Entries.universes_entry * bool * UState.t (** {6 Helpers to obtain proof state when in an interactive proof } *) |