aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/uState.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-03-11 01:14:28 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-30 17:50:37 +0200
commit0dc79e09b2b7c369b35191191aa257451a536540 (patch)
tree56ecf715bf703828818c31a2279718cc1e31d479 /engine/uState.ml
parent118d24281bc62bb7ff503abee56f156545eb9eea (diff)
[api] Remove deprecated objects in engine / interp / library
Diffstat (limited to 'engine/uState.ml')
-rw-r--r--engine/uState.ml3
1 files changed, 0 insertions, 3 deletions
diff --git a/engine/uState.ml b/engine/uState.ml
index 844eb390b..15cf4d4c1 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -663,6 +663,3 @@ let update_sigma_env uctx env =
let pr_weak prl {uctx_weak_constraints=weak} =
let open Pp in
prlist_with_sep fnl (fun (u,v) -> prl u ++ str " ~ " ++ prl v) (UPairSet.elements weak)
-
-(** Deprecated *)
-let normalize = minimize