From 0dc79e09b2b7c369b35191191aa257451a536540 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 11 Mar 2018 01:14:28 +0100 Subject: [api] Remove deprecated objects in engine / interp / library --- engine/evd.ml | 24 ------------------------ 1 file changed, 24 deletions(-) (limited to 'engine/evd.ml') diff --git a/engine/evd.ml b/engine/evd.ml index 78d5d4c8f..0c9c3a29b 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -132,8 +132,6 @@ end module Store = Store.Make () -type evar = Evar.t - let string_of_existential evk = "?X" ^ string_of_int (Evar.repr evk) type evar_body = @@ -1206,28 +1204,6 @@ module Monad = type unsolvability_explanation = SeveralInstancesFound of int -(** Deprecated *) -type evar_universe_context = UState.t -let empty_evar_universe_context = UState.empty -let union_evar_universe_context = UState.union -let evar_universe_context_set = UState.context_set -let evar_universe_context_constraints = UState.constraints -let evar_context_universe_context = UState.context -let evar_universe_context_of = UState.of_context_set -let evar_universe_context_subst = UState.subst -let add_constraints_context = UState.add_constraints -let constrain_variables = UState.constrain_variables -let evar_universe_context_of_binders = UState.of_binders -let make_evar_universe_context e l = - let g = Environ.universes e in - match l with - | None -> UState.make g - | Some l -> UState.make_with_initial_binders g l -let normalize_evar_universe_context_variables = UState.normalize_variables -let abstract_undefined_variables = UState.abstract_undefined_variables -let normalize_evar_universe_context = UState.minimize -let nf_constraints = minimize_universes - module MiniEConstr = struct module ESorts = -- cgit v1.2.3