Chasing a few unsafe constr coercions.

2 files changed, 0 insertions, 42 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 6380e3fc1f..b30702d0d1 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -941,37 +941,8 @@ let universes evd = UState.ugraph evd.universes
 let update_sigma_env evd env =
   { evd with universes = UState.update_sigma_env evd.universes env }
 
-(* Conversion w.r.t. an evar map and its local universes. *)
-
-let test_conversion_gen env evd pb t u =
-  match pb with 
-  | Reduction.CONV -> 
-    Reduction.conv env
-      ~evars:((existential_opt_value evd), (UState.ugraph evd.universes))
-      t u
-  | Reduction.CUMUL -> Reduction.conv_leq env
-      ~evars:((existential_opt_value evd), (UState.ugraph evd.universes))
-      t u
-
-let test_conversion env d pb t u =
-  try test_conversion_gen env d pb t u; true
-  with _ -> false
-
 exception UniversesDiffer = UState.UniversesDiffer
 
-let eq_constr_univs evd t u =
-  let fold cstr sigma =
-    try Some (add_universe_constraints sigma cstr)
-    with Univ.UniverseInconsistency _ | UniversesDiffer -> None
-  in
-  match Universes.eq_constr_univs_infer (UState.ugraph evd.universes) fold t u evd with
-  | None -> evd, false
-  | Some evd -> evd, true
-
-let e_eq_constr_univs evdref t u =
-  let evd, b = eq_constr_univs !evdref t u in
-    evdref := evd; b
-
 (**********************************************************)
 (* Side effects *)
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 699b52c2b2..eeb9fd8618 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -569,19 +569,6 @@ val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor ->
 val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env ->
   evar_map -> Globnames.global_reference -> evar_map * constr
 
-(********************************************************************
-  Conversion w.r.t. an evar map, not unifying universes. See 
-  [Reductionops.infer_conv] for conversion up-to universes. *)
-
-val test_conversion : env -> evar_map -> conv_pb -> constr -> constr -> bool
-(** WARNING: This does not allow unification of universes *)
-
-val eq_constr_univs : evar_map -> constr -> constr -> evar_map * bool
-(** Syntactic equality up to universes, recording the associated constraints *)
-
-val e_eq_constr_univs : evar_map ref -> constr -> constr -> bool
-(** Syntactic equality up to universes. *)
-
 (********************************************************************)
 (* constr with holes and pending resolution of classes, conversion  *)
 (* problems, candidates, etc.                                       *)