3 files changed, 4 insertions, 11 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index ee03bc9007..4a103cdd23 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -15,6 +15,7 @@ open Nameops
 open Libnames
 open Pputils
 open Ppextend
+open Notation_term
 open Constrexpr
 open Constrexpr_ops
 open Decl_kinds
@@ -737,7 +738,7 @@ let tag_var = tag Tag.variable
     pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
   }
 
-  type precedence =  Ppextend.precedence * Ppextend.parenRelation
+  type precedence =  Notation_term.precedence * Notation_term.parenRelation
   let modular_constr_pr = pr
   let rec fix rf x = rf (fix rf) x
   let pr = fix modular_constr_pr mt
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 8335034851..7546c748d8 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -15,6 +15,7 @@ open Libnames
 open Constrexpr
 open Names
 open Misctypes
+open Notation_term
 
 val extract_lam_binders :
   constr_expr -> local_binder_expr list * constr_expr
@@ -24,7 +25,7 @@ val split_fix :
   int -> constr_expr -> constr_expr ->
   local_binder_expr list *  constr_expr * constr_expr
 
-val prec_less : int -> int * Ppextend.parenRelation -> bool
+val prec_less : precedence -> tolerability -> bool
 
 val pr_tight_coma : unit -> Pp.t
 
diff --git a/printing/printer.ml b/printing/printer.ml
index e9d104b491..28b10c7812 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -846,15 +846,6 @@ let pr_goal_by_uid uid =
 (* Elementary tactics *)
 
 let pr_prim_rule = function
-  | Cut (b,replace,id,t) ->
-     if b then
-       (* TODO: express "replace" *)
-       (str"assert " ++ str"(" ++ pr_id id ++ str":" ++ pr_lconstr t ++ str")")
-     else
-       let cl = if replace then str"clear " ++ pr_id id ++ str"; " else mt() in
-       (str"cut " ++ pr_constr t ++
-        str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]")
-
   | Refine c ->
       (** FIXME *)
       str(if Termops.occur_meta Evd.empty (EConstr.of_constr c) then "refine " else "exact ") ++