From 86952ac8ad1dba395cb4724ac0b4f54774448944 Mon Sep 17 00:00:00 2001 From: barras Date: Thu, 29 Nov 2001 09:21:25 +0000 Subject: nouvel algo de conversion plus uniforme git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/conv_oracle.mli | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 kernel/conv_oracle.mli (limited to 'kernel/conv_oracle.mli') diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli new file mode 100644 index 000000000..94da48d4d --- /dev/null +++ b/kernel/conv_oracle.mli @@ -0,0 +1,32 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* table_key -> bool + +(* Changing the oracle *) +val set_opaque_const : section_path -> unit +val set_transparent_const : section_path -> unit + +val set_opaque_var : identifier -> unit +val set_transparent_var : identifier -> unit + +(*****************************) + +(* transparent state summary operations *) +val init : unit -> unit +val freeze : unit -> transparent_state +val unfreeze : transparent_state -> unit -- cgit v1.2.3