diff options
Diffstat (limited to 'kernel/pre_env.mli')
| -rw-r--r-- | kernel/pre_env.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 9561333c8d..7ef2ab0098 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -54,7 +54,9 @@ type env = { env_nb_rel : int; env_stratification : stratification; env_conv_oracle : Conv_oracle.oracle; - retroknowledge : Retroknowledge.retroknowledge } + retroknowledge : Retroknowledge.retroknowledge; + indirect_pterms : Opaqueproof.opaquetab; +} type named_context_val = named_context * named_vals |