diff options
author | 2013-05-08 18:01:07 +0200 | |
---|---|---|
committer | 2013-05-08 18:01:07 +0200 | |
commit | 095eac936751bab72e3c6bbdfa3ede51f7198721 (patch) | |
tree | 44cf2859ba6b8486f056efaaf7ee6c2d855f2aae /kernel/conv_oracle.mli | |
parent | 4e6d6dab2ef2de6c1ad7972fc981e55a4fde7ae3 (diff) | |
parent | 0b14713e3efd7f8f1cc8a06555d0ec8fbe496130 (diff) |
Merge branch 'experimental/master'
Diffstat (limited to 'kernel/conv_oracle.mli')
-rw-r--r-- | kernel/conv_oracle.mli | 16 |
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 |