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.

---
 interp/constrarg.ml  | 6 +-----
 interp/constrarg.mli | 4 ----
 2 files changed, 1 insertion(+), 9 deletions(-)

(limited to 'interp')

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 4f20dd5606..846fb5b934 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 b83c20065d..1654d27194 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
-- 
cgit v1.2.3