From de2397e5ed4d050c8bc157803a0d8827b9b0caf9 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 23 Jul 2019 14:31:59 +0200
Subject: [funind] Remove single-shot type alias.

Pointed out by Gaëtan Gilbert.
---
 plugins/funind/g_indfun.mlg | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index a7ef5fe884..1b75d3d966 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -148,9 +148,7 @@ END
 module Vernac = Pvernac.Vernac_
 module Tactic = Pltac
 
-type function_rec_definition_loc_argtype = Vernacexpr.fixpoint_expr Loc.located
-
-let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genarg.uniform_genarg_type) =
+let (wit_function_rec_definition_loc : Vernacexpr.fixpoint_expr Loc.located Genarg.uniform_genarg_type) =
   Genarg.create_arg "function_rec_definition_loc"
 
 let function_rec_definition_loc =
-- 
cgit v1.2.3