Updated version 8.9.0 from 'upstream/8.9.0'

with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63

1 files changed, 5 insertions, 4 deletions

diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 643f7e99..35ed14fc 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 open Pp
+open Constr
 open Genarg
 open Stdarg
 open Pcoq.Prim
@@ -169,10 +170,10 @@ END
 
 
 TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x Term.DEFAULTcast ]
+| ["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
 
@@ -188,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
@@ -219,7 +220,7 @@ VERNAC COMMAND FUNCTIONAL EXTEND HintCut CLASSIFIED AS SIDEFF
     fun ~atts ~st -> begin
         let open Vernacinterp in
         let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
-        Hints.add_hints (Locality.make_section_locality atts.locality)
+        Hints.add_hints ~local:(Locality.make_section_locality atts.locality)
           (match dbnames with None -> ["core"] | Some l -> l) entry;
         st
       end