CLEANUP: in the Reduction module

4 files changed, 27 insertions, 54 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 425b67e08..206014164 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -926,10 +926,10 @@ let update_sigma_env evd env =
 let test_conversion_gen env evd pb t u =
   match pb with 
   | Reduction.CONV -> 
-    Reduction.trans_conv_universes 
+    Reduction.conv_universes 
       full_transparent_state ~evars:(existential_opt_value evd) env 
       (UState.ugraph evd.universes) t u
-  | Reduction.CUMUL -> Reduction.trans_conv_leq_universes
+  | Reduction.CUMUL -> Reduction.conv_leq_universes
      full_transparent_state ~evars:(existential_opt_value evd) env 
       (UState.ugraph evd.universes) t u
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 33beca28a..8c9be0edd 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -126,7 +126,7 @@ let whd_betadeltaiota_nolet env t =
 
 (* Conversion utility functions *)
 type 'a conversion_function = env -> 'a -> 'a -> unit
-type 'a trans_conversion_function = Names.transparent_state -> 'a conversion_function
+type 'a trans_conversion_function = ?reds:Names.transparent_state -> 'a conversion_function
 type 'a universe_conversion_function = env -> UGraph.t -> 'a -> 'a -> unit
 type 'a trans_universe_conversion_function = 
   Names.transparent_state -> 'a universe_conversion_function
@@ -616,7 +616,7 @@ let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare =
   { compare = infer_cmp_universes;
     compare_instances = infer_convert_instances }
 
-let trans_fconv_universes reds cv_pb l2r evars env univs t1 t2 =
+let fconv_universes reds cv_pb l2r evars env univs t1 t2 =
   let b = 
     if cv_pb = CUMUL then leq_constr_univs univs t1 t2 
     else eq_constr_univs univs t1 t2
@@ -627,38 +627,22 @@ let trans_fconv_universes reds cv_pb l2r evars env univs t1 t2 =
 	()
 
 (* Profiling *)
-let trans_fconv_universes = 
+let fconv_universes = 
   if Flags.profile then
-    let trans_fconv_universes_key = Profile.declare_profile "trans_fconv_universes" in
-      Profile.profile8 trans_fconv_universes_key trans_fconv_universes
-  else trans_fconv_universes
-
-let trans_fconv reds cv_pb l2r evars env = 
-  trans_fconv_universes reds cv_pb l2r evars env (universes env)
-
-let trans_conv_cmp ?(l2r=false) conv reds = trans_fconv reds conv l2r (fun _->None)
-let trans_conv ?(l2r=false) ?(evars=fun _->None) reds = trans_fconv reds CONV l2r evars
-let trans_conv_leq ?(l2r=false) ?(evars=fun _->None) reds = trans_fconv reds CUMUL l2r evars
-
-let trans_conv_universes ?(l2r=false) ?(evars=fun _->None) reds = 
-  trans_fconv_universes reds CONV l2r evars
-let trans_conv_leq_universes ?(l2r=false) ?(evars=fun _->None) reds = 
-  trans_fconv_universes reds CUMUL l2r evars
-
-let fconv = trans_fconv full_transparent_state
-
-let conv_cmp ?(l2r=false) cv_pb = fconv cv_pb l2r (fun _->None)
-let conv ?(l2r=false) ?(evars=fun _->None) = fconv CONV l2r evars
-let conv_leq ?(l2r=false) ?(evars=fun _->None) = fconv CUMUL l2r evars
-
-let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 =
-  Array.fold_left2_i
-    (fun i _ t1 t2 ->
-      try conv_leq ~l2r ~evars env t1 t2
-      with NotConvertible -> raise (NotConvertibleVect i))
-    ()
-    v1
-    v2
+    let fconv_universes_key = Profile.declare_profile "trans_fconv_universes" in
+      Profile.profile8 fconv_universes_key fconv_universes
+  else fconv_universes
+
+let fconv ?(reds=full_transparent_state) cv_pb l2r evars env = 
+  fconv_universes reds cv_pb l2r evars env (universes env)
+
+let conv ?(l2r=false) ?(evars=fun _->None) ?(reds=full_transparent_state) =
+  fconv ~reds CONV l2r evars
+
+let conv_universes ?(l2r=false) ?(evars=fun _->None) reds =
+  fconv_universes reds CONV l2r evars
+let conv_leq_universes ?(l2r=false) ?(evars=fun _->None) reds = 
+  fconv_universes reds CUMUL l2r evars
 
 let generic_conv cv_pb ~l2r evars reds env univs t1 t2 =
   let (s, _) = 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 7db7e57bb..304046a1d 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -27,7 +27,7 @@ exception NotConvertible
 exception NotConvertibleVect of int
 
 type 'a conversion_function = env -> 'a -> 'a -> unit
-type 'a trans_conversion_function = Names.transparent_state -> 'a conversion_function
+type 'a trans_conversion_function = ?reds:Names.transparent_state -> 'a conversion_function
 type 'a universe_conversion_function = env -> UGraph.t -> 'a -> 'a -> unit
 type 'a trans_universe_conversion_function = 
   Names.transparent_state -> 'a universe_conversion_function
@@ -58,25 +58,14 @@ val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t ->
 val checked_universes : UGraph.t universe_compare
 val inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare
 
-val trans_conv_cmp       : ?l2r:bool -> conv_pb -> constr trans_conversion_function
-val trans_conv           :
+val conv :
   ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_conversion_function
-val trans_conv_leq       :
-  ?l2r:bool -> ?evars:(existential->constr option) -> types trans_conversion_function
 
-val trans_conv_universes     :
+val conv_universes :
   ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_universe_conversion_function
-val trans_conv_leq_universes :
+val conv_leq_universes :
   ?l2r:bool -> ?evars:(existential->constr option) -> types trans_universe_conversion_function
 
-val conv_cmp       : ?l2r:bool -> conv_pb -> constr conversion_function
-val conv           :
-  ?l2r:bool -> ?evars:(existential->constr option) -> constr conversion_function
-val conv_leq       :
-  ?l2r:bool -> ?evars:(existential->constr option) -> types conversion_function
-val conv_leq_vecti :
-  ?l2r:bool -> ?evars:(existential->constr option) -> types array conversion_function
-
 (** These conversion functions are used by module subtyping, which needs to infer
     universe constraints inside the kernel *)
 val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index d5a93230f..03e7f2642 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1264,8 +1264,8 @@ let test_trans_conversion (f: ?l2r:bool-> ?evars:'a->'b) reds env sigma x y =
   with Reduction.NotConvertible -> false
     | e when is_anomaly e -> report_anomaly e
 
-let is_trans_conv reds env sigma = test_trans_conversion Reduction.trans_conv_universes reds env sigma
-let is_trans_conv_leq reds env sigma = test_trans_conversion Reduction.trans_conv_leq_universes reds env sigma
+let is_trans_conv reds env sigma = test_trans_conversion Reduction.conv_universes reds env sigma
+let is_trans_conv_leq reds env sigma = test_trans_conversion Reduction.conv_leq_universes reds env sigma
 let is_trans_fconv = function Reduction.CONV -> is_trans_conv | Reduction.CUMUL -> is_trans_conv_leq
 
 let is_conv = is_trans_conv full_transparent_state
@@ -1274,8 +1274,8 @@ let is_fconv = function | Reduction.CONV -> is_conv | Reduction.CUMUL -> is_conv
 
 let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = 
   let f = match pb with
-    | Reduction.CONV -> Reduction.trans_conv_universes
-    | Reduction.CUMUL -> Reduction.trans_conv_leq_universes 
+    | Reduction.CONV -> Reduction.conv_universes
+    | Reduction.CUMUL -> Reduction.conv_leq_universes 
   in
     try f ~evars:(safe_evar_value sigma) ts env (Evd.universes sigma) x y; true
     with Reduction.NotConvertible -> false