diff --git a/classical/contra.v b/classical/contra.v
index 6f158e482..e3e1ffe6c 100644
--- a/classical/contra.v
+++ b/classical/contra.v
@@ -746,76 +746,8 @@ Proof. by rewrite 2!lax_notE. Qed.
 
 End Internals.
 Import Internals.
-Canonical TypeForall.
-Canonical PropForall.
-Canonical SetForall.
-Canonical wrap1Prop.
-Canonical wrap1Type.
-Canonical proper_nProp.
-Canonical trivial_nProp.
-Canonical True_nProp.
-Canonical False_nProp.
-Canonical not_nProp.
-Canonical and_nProp.
-Canonical and3_nProp.
-Canonical and4_nProp.
-Canonical and5_nProp.
-Canonical or_nProp.
-Canonical or3_nProp.
-Canonical or4_nProp.
-Canonical unary_and_rhs.
-Canonical binary_and_rhs.
-Canonical imply_nProp.
-Canonical exists_nProp.
-Canonical exists2_nProp.
-Canonical inhabited_nProp.
-Canonical forall_nProp.
-Canonical proper_nBody.
-Canonical nonproper_nBody.
-Canonical bounded_nBody.
-Canonical unbounded_nBody.
-Canonical is_true_nProp.
-Canonical true_neg.
-Canonical true_pos.
-Canonical false_neg.
-Canonical false_pos.
-Canonical id_neg.
-Canonical id_pos.
-Canonical negb_neg.
-Canonical negb_pos.
-Canonical neg_ltn_LHS.
-Canonical neg_leq_LHS.
-Canonical leq_neg.
-Canonical eq_nProp.
-Canonical bool_neq.
-Canonical true_neq.
-Canonical false_neq.
-Canonical eqType_neq.
-Canonical eq_op_pos.
-Canonical Prop_wType.
-Canonical proper_wType.
-Canonical forall_wType.
-Canonical inhabited_wType.
-Canonical void_wType.
-Canonical unit_wType.
-Canonical pair_wType.
-Canonical sum_wType.
-Canonical sumbool_wType.
-Canonical sumor_wType.
-Canonical sig1_wType.
-Canonical sig2_wType.
-Canonical sigT_wType.
-Canonical sigT2_wType.
-Canonical proper_wProp.
-Canonical forall_wProp.
-Canonical trivial_wProp.
-Canonical inhabited_wProp.
-Canonical nand_false_bool.
-Canonical nand_true_bool.
-Canonical and_wProp.
-Canonical or_wProp.
-Canonical exists_wProp.
-Canonical exists2_wProp.
+Hint View for move/ move_viewP|2.
+Export (canonicals) Internals.
 
 (******************************************************************************)
 (* Lemma and tactic assume_not: add a goal negation assumption. The tactic    *)