4 files changed, 16 insertions, 5 deletions
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 9ecc36bdf3..3f2fabeeee 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -99,8 +99,19 @@ TACTIC EXTEND is_ground
 | [ "is_ground" constr(ty) ] -> { is_ground ty }
 END
 
+{
+let deprecated_autoapply_using =
+  CWarnings.create
+    ~name:"autoapply-using" ~category:"deprecated"
+    (fun () -> Pp.str "The syntax [autoapply ... using] is deprecated. Use [autoapply ... with] instead.")
+}
+
 TACTIC EXTEND autoapply
-| [ "autoapply" constr(c) "using" preident(i) ] -> { autoapply c i }
+| [ "autoapply" constr(c) "using" preident(i) ] -> {
+    deprecated_autoapply_using ();
+    autoapply c i
+  }
+| [ "autoapply" constr(c) "with" preident(i) ] -> { autoapply c i }
 END
 
 {
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 7da4464e59..e78d0f93a4 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -449,7 +449,7 @@ let evd_convertible env evd x y =
        unsolvable constraints remain, so we check that this unification
        does not introduce any new problem. *)
     let _, pbs = Evd.extract_all_conv_pbs evd in
-    let evd' = Evarconv.the_conv_x env x y evd in
+    let evd' = Evarconv.unify_delay env evd x y in
     let _, pbs' = Evd.extract_all_conv_pbs evd' in
     if evd' == evd || problem_inclusion pbs' pbs then Some evd'
     else None
@@ -1989,7 +1989,7 @@ let add_morphism_infer atts m n =
 	Decl_kinds.DefinitionBody Decl_kinds.Instance 
       in
       let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
-      let hook _ = function
+      let hook _ _ _ = function
 	| Globnames.ConstRef cst ->
 	  add_instance (Typeclasses.new_instance 
 			  (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index a1e21aab04..543d4de0fe 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -557,7 +557,7 @@ let rec intern_atomic lf ist x =
       | _ -> false
       in
       let is_onconcl = match cl.concl_occs with
-      | AllOccurrences | NoOccurrences -> true
+      | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true
       | _ -> false
       in
       TacChange (None,
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 30f716d764..eac84f0543 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1766,7 +1766,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
           | _ -> false
         in
         let is_onconcl = match cl.concl_occs with
-          | AllOccurrences | NoOccurrences -> true
+          | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true
           | _ -> false
         in
         let c_interp patvars env sigma =