From 82b959a8f6025f84a39efb67985e6fe1a338b94b Mon Sep 17 00:00:00 2001 From: barras Date: Wed, 21 May 2008 23:25:22 +0000 Subject: refined the conversion oracle git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10960 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/redexpr.mli | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) (limited to 'proofs/redexpr.mli') diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli index fee3f9813..404a8a196 100644 --- a/proofs/redexpr.mli +++ b/proofs/redexpr.mli @@ -25,13 +25,8 @@ val reduction_of_red_expr : red_expr -> reduction_function * cast_kind val declare_red_expr : string -> reduction_function -> unit (* Opaque and Transparent commands. *) -val set_opaque_const : constant -> unit -val set_transparent_const : constant -> unit - -val set_opaque_var : identifier -> unit -val set_transparent_var : identifier -> unit - +val set_strategy : 'a tableKey -> Conv_oracle.level -> unit (* call by value normalisation function using the virtual machine *) val cbv_vm : reduction_function -- cgit v1.2.3