diff options
| author | Emilio Jesus Gallego Arias | 2020-04-02 01:46:07 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-15 11:12:14 -0400 |
| commit | 813da65015ce35c98a9203af6ad5099e587992a5 (patch) | |
| tree | 7d6f8a133f47e122a0905f2debd5d49f5e58cbb7 /dev/doc | |
| parent | 0c748e670ef1a81cb35c1cc55892dba141c25930 (diff) | |
[proof] [abstract] Move internal declaration code to `Declare`
As we are aiming to forbid low-level manipulation of proofs outside
`Declare`, we move the code from `Abstract` to `Declare`.
We remove `build_constant_by_tactic` from the public API.
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions