Merge PR #6098: [api] Move structures deprecated in the API to the core.

1 files changed, 4 insertions, 4 deletions

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 28a13fb404..38460c669f 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1120,10 +1120,10 @@ let pr_goal_selector ~toplevel s =
     let ty = EConstr.Unsafe.to_constr ty in
     let rec strip_ty acc n ty =
       if n=0 then (List.rev acc, EConstr.of_constr ty) else
-        match Term.kind_of_term ty with
-            Term.Prod(na,a,b) ->
-              strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b
-          | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
+        match Constr.kind ty with
+        | Constr.Prod(na,a,b) ->
+          strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b
+        | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
     strip_ty [] n ty
 
   let pr_atomic_tactic_level env sigma n t =