From 9c6487ba87f448daa28158c6e916e3d932c50645 Mon Sep 17 00:00:00 2001 From: barras Date: Wed, 20 Oct 2004 13:50:08 +0000 Subject: COMMITED BYTECODE COMPILER git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/conv_oracle.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/conv_oracle.mli') diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index 8dad2e2bd..351df9d86 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -9,13 +9,13 @@ (* $Id$ *) open Names -open Closure + (* 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 : table_key -> table_key -> bool +val oracle_order : 'a tableKey -> 'a tableKey -> bool (* Changing the oracle *) val set_opaque_const : kernel_name -> unit -- cgit v1.2.3