From 88fe0bcf86ad6cb95ffacfcd37f51fa3ae2da4fc Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 13 Nov 2019 15:50:39 +0100
Subject: Remove deprecated compat modifier of Notation / Infix commands.

And simplify a lot the compatibility infrastructure following this.

Update dev/tools/update-compat.py

Remove much complexity.

Co-authored-by: Jason Gross <jgross@mit.edu>
---
 lib/flags.ml | 30 ------------------------------
 1 file changed, 30 deletions(-)

(limited to 'lib/flags.ml')

diff --git a/lib/flags.ml b/lib/flags.ml
index 27ca8e9596..b87ba46634 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -57,36 +57,6 @@ let raw_print = ref false
 
 let we_are_parsing = ref false
 
-(* Compatibility mode *)
-
-(* Current means no particular compatibility consideration.
-   For correct comparisons, this constructor should remain the last one. *)
-
-type compat_version = V8_9 | V8_10 | V8_11 | Current
-
-let compat_version = ref Current
-
-let version_compare v1 v2 = match v1, v2 with
-  | V8_9, V8_9 -> 0
-  | V8_9, _ -> -1
-  | _, V8_9 -> 1
-  | V8_10, V8_10 -> 0
-  | V8_10, _ -> -1
-  | _, V8_10 -> 1
-  | V8_11, V8_11 -> 0
-  | V8_11, _ -> -1
-  | _, V8_11 -> 1
-  | Current, Current -> 0
-
-let version_strictly_greater v = version_compare !compat_version v > 0
-let version_less_or_equal v = not (version_strictly_greater v)
-
-let pr_version = function
-  | V8_9 -> "8.9"
-  | V8_10 -> "8.10"
-  | V8_11 -> "8.11"
-  | Current -> "current"
-
 (* Translate *)
 let beautify = ref false
 let beautify_file = ref false
-- 
cgit v1.2.3