Removing the useless pattern ident genarg.

11 files changed, 23 insertions, 33 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 934b9b117..093a561d6 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -31,7 +31,7 @@ let mk_extraarg loc s =
 
 let rec make_wit loc = function
   | IntOrVarArgType -> <:expr< Constrarg.wit_int_or_var >>
-  | IdentArgType b -> <:expr< Constrarg.wit_ident_gen $mlexpr_of_bool b$ >>
+  | IdentArgType -> <:expr< Constrarg.wit_ident >>
   | VarArgType -> <:expr< Constrarg.wit_var >>
   | QuantHypArgType -> <:expr< Constrarg.wit_quant_hyp >>
   | GenArgType -> <:expr< Constrarg.wit_genarg >>
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 3e11bf5a8..b3f60dee6 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -203,7 +203,7 @@ let mlexpr_of_red_expr = function
 
 let rec mlexpr_of_argtype loc = function
   | Genarg.IntOrVarArgType -> <:expr< Genarg.IntOrVarArgType >>
-  | Genarg.IdentArgType b -> <:expr< Genarg.IdentArgType $mlexpr_of_bool b$ >>
+  | Genarg.IdentArgType -> <:expr< Genarg.IdentArgType >>
   | Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
   | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >>
   | Genarg.OpenConstrArgType -> <:expr< Genarg.OpenConstrArgType >>
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 4f20dd560..846fb5b93 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -39,11 +39,7 @@ let wit_intro_pattern : intro_pattern_expr located uniform_genarg_type =
 let wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type =
   Genarg.make0 None "tactic"
 
-let wit_ident_gen b = unsafe_of_type (IdentArgType b)
-
-let wit_ident = wit_ident_gen true
-
-let wit_pattern_ident = wit_ident_gen false
+let wit_ident = unsafe_of_type IdentArgType
 
 let wit_var = unsafe_of_type VarArgType
 
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index b83c20065..1654d2719 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -36,10 +36,6 @@ val wit_intro_pattern : intro_pattern_expr located uniform_genarg_type
 
 val wit_ident : Id.t uniform_genarg_type
 
-val wit_pattern_ident : Id.t uniform_genarg_type
-
-val wit_ident_gen : bool -> Id.t uniform_genarg_type
-
 val wit_var : (Id.t located, Id.t located, Id.t) genarg_type
 
 val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type
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"
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 51c261742..f275b0d00 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -191,7 +191,7 @@ val app_pair :
 type argument_type =
   (** Basic types *)
   | IntOrVarArgType
-  | IdentArgType of bool
+  | IdentArgType
   | VarArgType
   (** Specific types *)
   | GenArgType
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index d25efa72a..e26ecbea3 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -322,7 +322,7 @@ module Prim =
 
     let name = Gram.entry_create "Prim.name"
     let identref = Gram.entry_create "Prim.identref"
-    let pattern_ident = gec_gen (rawwit wit_pattern_ident) "pattern_ident"
+    let pattern_ident = Gram.entry_create "pattern_ident"
     let pattern_identref = Gram.entry_create "pattern_identref"
 
     (* A synonym of ident - maybe ident will be located one day *)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index cb09784c1..ae3b41e23 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -141,12 +141,11 @@ let pr_fresh_ids = prlist (fun s -> spc() ++ pr_or_var qs s)
 
 let with_evars ev s = if ev then "e" ^ s else s
 
-let if_pattern_ident b pr c = (if b then str "?" else mt()) ++ pr c
 
 let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) =
   match Genarg.genarg_tag x with
   | IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x)
-  | IdentArgType b -> if_pattern_ident b pr_id (out_gen (rawwit wit_ident) x)
+  | IdentArgType -> pr_id (out_gen (rawwit wit_ident) x)
   | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x)
   | GenArgType -> pr_raw_generic prc prlc prtac prpat prref (out_gen (rawwit wit_genarg) x)
   | ConstrArgType -> prc (out_gen (rawwit wit_constr) x)
@@ -180,7 +179,7 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi
 let rec pr_glb_generic prc prlc prtac prpat x =
   match Genarg.genarg_tag x with
   | IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x)
-  | IdentArgType b -> if_pattern_ident b pr_id (out_gen (glbwit wit_ident) x)
+  | IdentArgType -> pr_id (out_gen (glbwit wit_ident) x)
   | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x)
   | GenArgType -> pr_glb_generic prc prlc prtac prpat (out_gen (glbwit wit_genarg) x)
   | ConstrArgType -> prc (out_gen (glbwit wit_constr) x)
@@ -215,7 +214,7 @@ let rec pr_glb_generic prc prlc prtac prpat x =
 let rec pr_top_generic prc prlc prtac prpat x =
   match Genarg.genarg_tag x with
   | IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x)
-  | IdentArgType b -> if_pattern_ident b pr_id (out_gen (topwit wit_ident) x)
+  | IdentArgType -> pr_id (out_gen (topwit wit_ident) x)
   | VarArgType -> pr_id (out_gen (topwit wit_var) x)
   | GenArgType -> pr_top_generic prc prlc prtac prpat (out_gen (topwit wit_genarg) x)
   | ConstrArgType -> prc (out_gen (topwit wit_constr) x)
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 7f676c157..c787ebbda 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -714,10 +714,10 @@ and intern_genarg ist x =
   | IntOrVarArgType ->
       in_gen (glbwit wit_int_or_var)
         (intern_or_var ist (out_gen (rawwit wit_int_or_var) x))
-  | IdentArgType b ->
+  | IdentArgType ->
       let lf = ref Id.Set.empty in
-      in_gen (glbwit (wit_ident_gen b))
-	(intern_ident lf ist (out_gen (rawwit (wit_ident_gen b)) x))
+      in_gen (glbwit wit_ident)
+	(intern_ident lf ist (out_gen (rawwit wit_ident) x))
   | VarArgType ->
       in_gen (glbwit wit_var) (intern_hyp ist (out_gen (rawwit wit_var) x))
   | GenArgType ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 16fc73cfd..b697d3635 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1327,9 +1327,9 @@ and interp_genarg ist env sigma concl gl x =
     | IntOrVarArgType ->
       in_gen (topwit wit_int_or_var)
         (ArgArg (interp_int_or_var ist (out_gen (glbwit wit_int_or_var) x)))
-    | IdentArgType b ->
-      in_gen (topwit (wit_ident_gen b))
-        (interp_fresh_ident ist env (out_gen (glbwit (wit_ident_gen b)) x))
+    | IdentArgType ->
+      in_gen (topwit wit_ident)
+        (interp_fresh_ident ist env (out_gen (glbwit wit_ident) x))
     | VarArgType ->
       in_gen (topwit wit_var) (interp_hyp ist env (out_gen (glbwit wit_var) x))
     | GenArgType ->
@@ -1981,10 +1981,10 @@ and interp_atomic ist tac =
         match tag with
           | IntOrVarArgType ->
               (Proofview.Goal.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x)))
-          | IdentArgType b ->
+          | IdentArgType ->
               Proofview.Goal.lift begin
 	        Goal.return (value_of_ident (interp_fresh_ident ist env
-	                                       (out_gen (glbwit (wit_ident_gen b)) x)))
+	                                       (out_gen (glbwit wit_ident) x)))
               end
           | VarArgType ->
               Proofview.Goal.return (mk_hyp_value ist env (out_gen (glbwit wit_var) x))
@@ -2025,8 +2025,8 @@ and interp_atomic ist tac =
               let wit = glbwit (wit_list wit_int_or_var) in
               let ans = List.map (mk_int_or_var_value ist) (out_gen wit x) in
               (Proofview.Goal.return (in_gen (topwit (wit_list wit_genarg)) ans))
-          | ListArgType (IdentArgType b) ->
-              let wit = glbwit (wit_list (wit_ident_gen b)) in
+          | ListArgType IdentArgType ->
+              let wit = glbwit (wit_list wit_ident) in
 	      let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in
 	      let ans = List.map mk_ident (out_gen wit x) in
               (Proofview.Goal.return (in_gen (topwit (wit_list wit_genarg)) ans))
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 206dec104..d3cc6adc5 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -295,8 +295,8 @@ and subst_match_rule subst = function
 and subst_genarg subst (x:glob_generic_argument) =
   match genarg_tag x with
   | IntOrVarArgType -> in_gen (glbwit wit_int_or_var) (out_gen (glbwit wit_int_or_var) x)
-  | IdentArgType b ->
-      in_gen (glbwit (wit_ident_gen b)) (out_gen (glbwit (wit_ident_gen b)) x)
+  | IdentArgType ->
+      in_gen (glbwit wit_ident) (out_gen (glbwit wit_ident) x)
   | VarArgType -> in_gen (glbwit wit_var) (out_gen (glbwit wit_var) x)
   | GenArgType -> in_gen (glbwit wit_genarg) (subst_genarg subst (out_gen (glbwit wit_genarg) x))
   | ConstrArgType ->