3 files changed, 5 insertions, 4 deletions
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 3f2fabeeee..049a699cbd 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -84,7 +84,7 @@ TACTIC EXTEND typeclasses_eauto
  | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
     { typeclasses_eauto ~depth:d l }
  | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> {
-     typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] }
+     typeclasses_eauto ~only_classes:true ~depth:d [Class_tactics.typeclasses_db] }
 END
 
 TACTIC EXTEND head_of_constr
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 7bf705ffeb..a2dd51643b 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -72,7 +72,7 @@ let test_lpar_idnum_coloneq =
       match stream_nth 0 strm with
         | KEYWORD "(" ->
             (match stream_nth 1 strm with
-              | IDENT _ | INT _ ->
+              | IDENT _ | NUMERAL _ ->
                   (match stream_nth 2 strm with
                     | KEYWORD ":=" -> ()
                     | _ -> err ())
@@ -147,7 +147,8 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
     end
   | _ -> ElimOnConstr clbind
 
-let mkNumeral n = Numeral (string_of_int (abs n), 0<=n)
+let mkNumeral n =
+  Numeral ((if 0<=n then SPlus else SMinus),NumTok.int (string_of_int (abs n)))
 
 let mkTacCase with_evar = function
   | [(clear,ElimOnConstr cl),(None,None),None],None ->
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index b770b97384..814be64f81 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -48,7 +48,7 @@ let atactic n =
   else Aentryl (Pltac.tactic_expr, string_of_int n)
 
 type entry_name = EntryName :
-  'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name
+  'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Extend.symbol -> entry_name
 
 (** Quite ad-hoc *)
 let get_tacentry n m =