diff options
Diffstat (limited to 'kernel/conv_oracle.mli')
| -rw-r--r-- | kernel/conv_oracle.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index 94da48d4d..20ec5239e 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -12,7 +12,7 @@ open Names open Closure (* Order on section paths for unfolding. - If oracle_order sp1 sp2 is true, then unfold sp1 first. + If [oracle_order sp1 sp2] is true, then unfold sp1 first. Note: the oracle does not introduce incompleteness, it only tries to postpone unfolding of "opaque" constants. *) val oracle_order : table_key -> table_key -> bool |