summaryrefslogtreecommitdiff
path: root/kernel/conv_oracle.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/conv_oracle.mli')
-rw-r--r--kernel/conv_oracle.mli16
1 files changed, 7 insertions, 9 deletions
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 9272dfe5..f875fabf 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -1,22 +1,20 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: conv_oracle.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
open Names
-(* Order on section paths for unfolding.
+(** Order on section paths for unfolding.
If [oracle_order kn1 kn2] is true, then unfold kn1 first.
Note: the oracle does not introduce incompleteness, it only
tries to postpone unfolding of "opaque" constants. *)
-val oracle_order : 'a tableKey -> 'a tableKey -> bool
+val oracle_order : bool -> 'a tableKey -> 'a tableKey -> bool
-(* Priority for the expansion of constant in the conversion test.
+(** Priority for the expansion of constant in the conversion test.
* Higher levels means that the expansion is less prioritary.
* (And Expand stands for -oo, and Opaque +oo.)
* The default value (transparent constants) is [Level 0].
@@ -26,14 +24,14 @@ val transparent : level
val get_strategy : 'a tableKey -> level
-(* Sets the level of a constant.
+(** Sets the level of a constant.
* Level of RelKey constant cannot be set. *)
val set_strategy : 'a tableKey -> level -> unit
val get_transp_state : unit -> transparent_state
-(*****************************)
-(* Summary operations *)
+(****************************
+ Summary operations *)
type oracle
val init : unit -> unit
val freeze : unit -> oracle