deplacements des var. ex. hors du noyau

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@93 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 33 insertions, 44 deletions

diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 8b2d988c3a..f24431a2f7 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -8,7 +8,6 @@ open Term
 open Univ
 open Environ
 open Closure
-open Evd
 (*i*)
 
 (* Reduction Functions. *)
@@ -17,10 +16,10 @@ exception Redelimination
 exception Induc
 exception Elimconst
 
-type 'a reduction_function = 'a unsafe_env -> constr -> constr
+type 'a reduction_function = unsafe_env -> constr -> constr
 
 type 'a stack_reduction_function = 
-    'a unsafe_env -> constr -> constr list -> constr * constr list
+    unsafe_env -> constr -> constr list -> constr * constr list
 
 val whd_stack : 'a stack_reduction_function
 
@@ -73,41 +72,31 @@ val whd_betadeltaiotaeta : 'a reduction_function
 val beta_applist : (constr * constr list) -> constr
 
 
-(*s Special-Purpose Reduction Functions *)
-val whd_meta : 'a reduction_function
-val plain_instance : 'a reduction_function
-val instance : 'a reduction_function
-
-val whd_ise : 'a reduction_function
-val whd_ise1 : 'a reduction_function
-val nf_ise1 : 'a reduction_function
-val whd_ise1_metas : 'a reduction_function
-
-val hnf_prod_app : 'c unsafe_env -> string -> constr -> constr -> constr
+val hnf_prod_app : unsafe_env -> string -> constr -> constr -> constr
 val hnf_prod_appvect : 
-  'c unsafe_env -> string -> constr -> constr array -> constr
+  unsafe_env -> string -> constr -> constr array -> constr
 val hnf_prod_applist : 
-  'c unsafe_env -> string -> constr -> constr list -> constr
+  unsafe_env -> string -> constr -> constr list -> constr
 val hnf_lam_app : 
-  'c unsafe_env -> string -> constr -> constr -> constr
+  unsafe_env -> string -> constr -> constr -> constr
 val hnf_lam_appvect : 
-  'c unsafe_env -> string -> constr -> constr array -> constr
+  unsafe_env -> string -> constr -> constr array -> constr
 val hnf_lam_applist : 
-  'c unsafe_env -> string -> constr -> constr list -> constr
-val splay_prod : 'c unsafe_env -> constr -> (name * constr) list * constr
-val decomp_prod : 'c unsafe_env -> constr -> int * constr
+  unsafe_env -> string -> constr -> constr list -> constr
+val splay_prod : unsafe_env -> constr -> (name * constr) list * constr
+val decomp_prod : unsafe_env -> constr -> int * constr
 val decomp_n_prod : 
-  'c unsafe_env -> int -> constr -> ((name * constr) list) * constr
-
-val is_arity : 'c unsafe_env -> constr -> bool
-val is_info_arity : 'c unsafe_env -> constr -> bool
-val is_info_sort : 'c unsafe_env -> constr -> bool
-val is_logic_arity : 'c unsafe_env -> constr -> bool
-val is_type_arity : 'c unsafe_env -> constr -> bool
-val is_info_type : 'c unsafe_env -> typed_type -> bool
-val is_info_cast_type : 'c unsafe_env -> constr -> bool
-val contents_of_cast_type : 'c unsafe_env -> constr -> contents
-val poly_args : 'a unsafe_env -> constr -> int list
+  unsafe_env -> int -> constr -> ((name * constr) list) * constr
+
+val is_arity : unsafe_env -> constr -> bool
+val is_info_arity : unsafe_env -> constr -> bool
+val is_info_sort : unsafe_env -> constr -> bool
+val is_logic_arity : unsafe_env -> constr -> bool
+val is_type_arity : unsafe_env -> constr -> bool
+val is_info_type : unsafe_env -> typed_type -> bool
+val is_info_cast_type : unsafe_env -> constr -> bool
+val contents_of_cast_type : unsafe_env -> constr -> contents
+val poly_args : unsafe_env -> constr -> int list
 
 val whd_programs : 'a reduction_function
 
@@ -142,7 +131,7 @@ val convert_or : conversion_test -> conversion_test -> conversion_test
 val convert_forall2 : 
   ('a -> 'b -> conversion_test) -> 'a array -> 'b array -> conversion_test
 
-type 'a conversion_function = 'a unsafe_env -> constr -> constr -> constraints
+type 'a conversion_function = unsafe_env -> constr -> constr -> constraints
 
 val fconv : conv_pb -> 'a conversion_function
 
@@ -153,27 +142,27 @@ val conv : 'a conversion_function
 val conv_leq : 'a conversion_function
 
 val conv_forall2 : 
-  'a conversion_function -> 'a unsafe_env 
+  'a conversion_function -> unsafe_env 
     -> constr array -> constr array -> constraints
 
 val conv_forall2_i : 
-  (int -> 'a conversion_function) -> 'a unsafe_env 
+  (int -> 'a conversion_function) -> unsafe_env 
     -> constr array -> constr array -> constraints
 
-val is_conv : 'a unsafe_env -> constr -> constr -> bool
-val is_conv_leq : 'a unsafe_env -> constr -> constr -> bool
+val is_conv : unsafe_env -> constr -> constr -> bool
+val is_conv_leq : unsafe_env -> constr -> constr -> bool
 
 (*s Obsolete Reduction Functions *)
 
-val hnf : 'a unsafe_env -> constr -> constr * constr list
+val hnf : unsafe_env -> constr -> constr * constr list
 val apprec : 'a stack_reduction_function
 val red_product : 'a reduction_function
-val find_mrectype : 'a unsafe_env -> constr -> constr * constr list
-val find_minductype : 'a unsafe_env -> constr -> constr * constr list
-val find_mcoinductype : 'a unsafe_env -> constr -> constr * constr list
-val check_mrectype_spec : 'a unsafe_env -> constr -> constr
-val minductype_spec : 'a unsafe_env -> constr -> constr
-val mrectype_spec : 'a unsafe_env -> constr -> constr
+val find_mrectype : unsafe_env -> constr -> constr * constr list
+val find_minductype : unsafe_env -> constr -> constr * constr list
+val find_mcoinductype : unsafe_env -> constr -> constr * constr list
+val check_mrectype_spec : unsafe_env -> constr -> constr
+val minductype_spec : unsafe_env -> constr -> constr
+val mrectype_spec : unsafe_env -> constr -> constr
 
 (* Special function, which keep the key casts under Fix and MutCase. *)
 val strip_all_casts : constr -> constr