diff options
| author | Emilio Jesus Gallego Arias | 2019-07-17 08:41:52 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-31 11:13:05 +0200 |
| commit | 253bfe33f401212b1db29386e52572899905aa18 (patch) | |
| tree | a091631fa0b201aaaea7c40436b8486eef5ce801 /doc/plugin_tutorial/tuto2/src/custom.ml | |
| parent | eb6a7c1aaebe8bd777e03439666b8b2c18db5cd3 (diff) | |
[funind] Remove export of `generate_functional_principle` and `make_scheme`
This removes the export of two internal functions, moving to their
only use place.
In particular, `make_scheme` was exposing the low-level `proof_entry`
object, which should not do.
This will allow to refactor all these constant-building functions
towards a more uniform use of the API. In particular, all the
functions manipulating proof entries directly are in `Gen_principle`.
Diffstat (limited to 'doc/plugin_tutorial/tuto2/src/custom.ml')
0 files changed, 0 insertions, 0 deletions