diff options
Diffstat (limited to 'kernel/names.mli')
| -rw-r--r-- | kernel/names.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index 340f6e812..b19f93e2d 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -172,6 +172,7 @@ type transparent_state = Idpred.t * Cpred.t val empty_transparent_state : transparent_state val full_transparent_state : transparent_state val var_full_transparent_state : transparent_state +val cst_full_transparent_state : transparent_state type inv_rel_key = int (* index in the [rel_context] part of environment starting by the end, {\em inverse} |