diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-24 12:13:04 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-24 12:25:00 +0200 |
| commit | 2739fe8a22a9df48e717583d6efabc42e41f9814 (patch) | |
| tree | 9b354c954a43cc502c9d78d6c35f6942d55e480a /kernel/environ.mli | |
| parent | c6863a4cf8a9ec4bc91335f59f3094974f01dd13 (diff) | |
Make the retroknowledge marshalable.
Essential for parallel processing of Coq documents.
It is a fairly straightforward change but a tad tedious, I may have introduced some bugs in the process.
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 7f3fdc536..5e9e5264d 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -284,8 +284,6 @@ val retroknowledge : (retroknowledge->'a) -> env -> 'a val registered : env -> field -> bool -val unregister : env -> field -> env - val register : env -> field -> Retroknowledge.entry -> env (** Native compiler *) |