diff options
| author | Guillaume Melquiond | 2021-02-19 16:47:11 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2021-02-19 16:47:11 +0100 |
| commit | cec70c45e25d9a2a53ada7b9941b92663b08c7e0 (patch) | |
| tree | 022a274bb59b0614a8c71013301dc12297952286 /kernel/nativelambda.mli | |
| parent | b45ffd0bc0904e3d3325724e99b94239f5153b64 (diff) | |
Make most of DRealAbstr opaque.
The function returned by DRealAbstr starts by a call to the axiom
sig_forall_dec, so it is not computable anyway.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions