diff options
Diffstat (limited to 'plugins/funind/g_indfun.ml4')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index b5eacee81..5e6128b1b 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -23,8 +23,8 @@ open Pltac DECLARE PLUGIN "recdef_plugin" let pr_binding prc = function - | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) - | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) + | loc, (NamedHyp id, c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) + | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) let pr_bindings prc prlc = function | ImplicitBindings l -> @@ -158,7 +158,7 @@ GEXTEND Gram GLOBAL: function_rec_definition_loc ; function_rec_definition_loc: - [ [ g = Vernac.rec_definition -> !@loc, g ]] + [ [ g = Vernac.rec_definition -> Loc.tag ~loc:!@loc g ]] ; END |