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.mli | 4 ---- 1 file changed, 4 deletions(-) (limited to 'interp/constrarg.mli') 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 -- cgit v1.2.3