diff options
Diffstat (limited to 'plugins/ltac/g_auto.ml4')
| -rw-r--r-- | plugins/ltac/g_auto.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 642e52155..35ed14fc1 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -173,7 +173,7 @@ TACTIC EXTEND convert_concl_no_check | ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x DEFAULTcast ] END -let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_reference +let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_qualid let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global let glob_hints_path_atom ist = Hints.glob_hints_path_atom @@ -189,7 +189,7 @@ ARGUMENT EXTEND hints_path_atom END let pr_hints_path prc prx pry c = Hints.pp_hints_path c -let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_reference c +let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_qualid c let glob_hints_path ist = Hints.glob_hints_path ARGUMENT EXTEND hints_path |