aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/genarg.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2013-12-19 20:02:39 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2013-12-19 20:10:23 +0100
commit631298df172c1e034d6898ff13d5d5aabb9a5098 (patch)
treeb43a195fe510f6692aa5b17c48358a630f04cb1b /lib/genarg.ml
parentcfeb55070713c8131ca0f95c6c374c624b36a895 (diff)
Removing the useless pattern ident genarg.
Diffstat (limited to 'lib/genarg.ml')
-rw-r--r--lib/genarg.ml7
1 files changed, 3 insertions, 4 deletions
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 6520669fa..3fb815510 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -12,7 +12,7 @@ open Util
type argument_type =
(* Basic types *)
| IntOrVarArgType
- | IdentArgType of bool
+ | IdentArgType
| VarArgType
(* Specific types *)
| GenArgType
@@ -30,7 +30,7 @@ type argument_type =
let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
| IntOrVarArgType, IntOrVarArgType -> true
-| IdentArgType b1, IdentArgType b2 -> (b1 : bool) == b2
+| IdentArgType, IdentArgType -> true
| VarArgType, VarArgType -> true
| GenArgType, GenArgType -> true
| ConstrArgType, ConstrArgType -> true
@@ -49,8 +49,7 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
let rec pr_argument_type = function
| IntOrVarArgType -> str "int_or_var"
-| IdentArgType true -> str "ident"
-| IdentArgType false -> str "pattern_ident"
+| IdentArgType -> str "ident"
| VarArgType -> str "var"
| GenArgType -> str "genarg"
| ConstrArgType -> str "constr"