diff options
| author | Emilio Jesus Gallego Arias | 2019-07-23 14:31:59 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-23 14:31:59 +0200 |
| commit | de2397e5ed4d050c8bc157803a0d8827b9b0caf9 (patch) | |
| tree | 69949ee40a7fab42c3e63dcacff2ebe2586b6aca /plugins/funind | |
| parent | d407d1f3f2f877fca8673eaf0470b3390e55dbaa (diff) | |
[funind] Remove single-shot type alias.
Pointed out by Gaëtan Gilbert.
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/g_indfun.mlg | 4 |
1 files changed, 1 insertions, 3 deletions
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 = |