aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evd.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-11-29 17:49:11 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-02-14 17:30:44 +0100
commit390fd4ac0a969103caeb5db3e5138e26f9a533de (patch)
treef04f87b0fca81518797dabd0f9d2d395ba8ec2b8 /engine/evd.ml
parentd549d9d3d169fbfc5f555e3e4f22f46301161d53 (diff)
Chasing a few unsafe constr coercions.
Diffstat (limited to 'engine/evd.ml')
-rw-r--r--engine/evd.ml29
1 files changed, 0 insertions, 29 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index 6380e3fc1..b30702d0d 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 *)