From 631298df172c1e034d6898ff13d5d5aabb9a5098 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 19 Dec 2013 20:02:39 +0100
Subject: Removing the useless pattern ident genarg.

---
 grammar/argextend.ml4 | 2 +-
 grammar/q_coqast.ml4  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'grammar')

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 934b9b1173..093a561d6e 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 3e11bf5a8a..b3f60dee6a 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 >>
-- 
cgit v1.2.3