diff options
| author | Matthieu Sozeau | 2016-05-31 16:24:15 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-09 18:56:41 +0200 |
| commit | 55cd7e662ecdcf0f82bc76bdff2ad28f2cdef01c (patch) | |
| tree | 55501954dd115a91d154f49259ef4a0fee078a38 /kernel/closure.mli | |
| parent | 7527751d9772656b4680df311546825cc2dd3d8f (diff) | |
newring: fix for hack using evars as integers.
Diffstat (limited to 'kernel/closure.mli')
| -rw-r--r-- | kernel/closure.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/closure.mli b/kernel/closure.mli index 07176cb7de..8e172290fb 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -164,6 +164,9 @@ val inject : constr -> fconstr (** mk_atom: prevents a term from being evaluated *) val mk_atom : constr -> fconstr +(** mk_red: makes a reducible term (used in newring) *) +val mk_red : fterm -> fconstr + val fterm_of : fconstr -> fterm val term_of_fconstr : fconstr -> constr val destFLambda : |