diff --git a/qc-current/QC.v b/qc-current/QC.v
index 9dd674bad..877117487 100644
--- a/qc-current/QC.v
+++ b/qc-current/QC.v
@@ -1289,7 +1289,7 @@ End DefineGenSized.
     [QuickChick] provides some automation for deriving such instances
     for simple datatypes automatically! *)
 
-Derive Arbitrary for Tree.
+QCDerive Arbitrary for Tree.
 (**
 
      ===> GenSizedree is defined
@@ -1298,7 +1298,7 @@ Derive Arbitrary for Tree.
 Print GenSizedTree.
 Print ShrinkTree.
 
-Derive Show for Tree.
+QCDerive Show for Tree.
 (**
      ===> ShowTree is defined
 *)
diff --git a/qc-current/QuickChickTool.v b/qc-current/QuickChickTool.v
index 8a4d4bc7d..8f2b23fcd 100644
--- a/qc-current/QuickChickTool.v
+++ b/qc-current/QuickChickTool.v
@@ -126,7 +126,7 @@ Inductive exp : Type :=
 (** Since [exp] is a simple datatype, QuickChick can derive a generator, a
     shrinker, and a printer automatically. *)
 
-Derive (Arbitrary, Show) for exp.
+QCDerive (Arbitrary, Show) for exp.
 
 (** The [eval] function evaluates an expression to a number. *)
 Fixpoint eval (e : exp) : nat :=
diff --git a/qc-current/TImp.v b/qc-current/TImp.v
index 780fc3975..7bc2d5d25 100644
--- a/qc-current/TImp.v
+++ b/qc-current/TImp.v
@@ -136,7 +136,7 @@ Inductive ty := TBool | TNat.
     QuickChick provides a top-level vernacular command to derive such
     instances. *)
 
-Derive (Arbitrary, Show) for ty.
+QCDerive (Arbitrary, Show) for ty.
 (* ==>
     GenSizedty is defined
     Shrinkty is defined
@@ -352,7 +352,7 @@ Inductive exp : Type :=
 
 (** To print expressions we derive a [Show] Instance. *)
 
-Derive Show for exp.
+QCDerive Show for exp.
 
 (* ================================================================= *)
 (** ** Typed Expressions *)
@@ -699,7 +699,7 @@ Definition gen_typed_has_type :=
 
 Inductive value := VNat : nat -> value | VBool : bool -> value.
 
-Derive Show for value.
+QCDerive Show for value.
 
 (** We can also quickly define a typing relation for values, a Dec instance
     for it, and a generator for values of a given type. *)
@@ -862,7 +862,7 @@ Definition expression_soundness_exec :=
 (** Let's see what happens if we use the default shrinker for
     expressions carelessly. *)
 
-Derive Shrink for exp.
+QCDerive Shrink for exp.
 
 Definition expression_soundness_exec_firstshrink :=
   let num_vars := 4 in
@@ -1088,7 +1088,7 @@ Notation "'WHILE' b 'DO' c 'END'" :=
 Notation "'TEST' c1 'THEN' c2 'ELSE' c3 'FI'" :=
   (CIf c1 c2 c3) (at level 80, right associativity).
 
-Derive Show for com.
+QCDerive Show for com.
 
 (** (Of course, the derived [Show] instance is not going to use these
     notations!) *)
@@ -1296,7 +1296,7 @@ Conjecture well_typed_state_never_stuck :
     produce such generators -- i.e., generators for data structures
     satisfying inductively defined properties! *)
 
-Derive ArbitrarySizedSuchThat for (fun v => has_type_value v T).
+QCDerive ArbitrarySizedSuchThat for (fun v => has_type_value v T).
 (** ===>
   GenSizedSuchThathas_type_value is defined. *)
 
@@ -1345,7 +1345,7 @@ Print GenSizedSuchThathas_type_value.
 
 (** Moreover, QuickChick can also derive DecOpt instances automatically, as well as proofs of correctness! *)
 
-Derive DecOpt for (has_type_value v T).
+QCDerive DecOpt for (has_type_value v T).
 
 Print DecOpthas_type_value.