diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/names.ml | 1 | ||||
| -rw-r--r-- | kernel/names.mli | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index d1c6ee8a4..975390cb9 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -320,6 +320,7 @@ type transparent_state = Idpred.t * Cpred.t let empty_transparent_state = (Idpred.empty, Cpred.empty) let full_transparent_state = (Idpred.full, Cpred.full) let var_full_transparent_state = (Idpred.full, Cpred.empty) +let cst_full_transparent_state = (Idpred.empty, Cpred.full) type 'a tableKey = | ConstKey of constant 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} |