diff options
Diffstat (limited to 'parsing/extrawit.ml')
| -rw-r--r-- | parsing/extrawit.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml index 75205c964..be584b5c8 100644 --- a/parsing/extrawit.ml +++ b/parsing/extrawit.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors -open Util open Genarg (* This file defines extra argument types *) @@ -30,7 +28,7 @@ let wit_tactic = function | 3 -> wit_tactic3 | 4 -> wit_tactic4 | 5 -> wit_tactic5 - | n -> anomaly ("Unavailable tactic level: "^string_of_int n) + | n -> Errors.anomaly ("Unavailable tactic level: "^string_of_int n) let globwit_tactic = function | 0 -> globwit_tactic0 @@ -39,7 +37,7 @@ let globwit_tactic = function | 3 -> globwit_tactic3 | 4 -> globwit_tactic4 | 5 -> globwit_tactic5 - | n -> anomaly ("Unavailable tactic level: "^string_of_int n) + | n -> Errors.anomaly ("Unavailable tactic level: "^string_of_int n) let rawwit_tactic = function | 0 -> rawwit_tactic0 @@ -48,7 +46,7 @@ let rawwit_tactic = function | 3 -> rawwit_tactic3 | 4 -> rawwit_tactic4 | 5 -> rawwit_tactic5 - | n -> anomaly ("Unavailable tactic level: "^string_of_int n) + | n -> Errors.anomaly ("Unavailable tactic level: "^string_of_int n) let tactic_genarg_level s = if String.length s = 7 && String.sub s 0 6 = "tactic" then |