3 files changed, 10 insertions, 4 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index e39d17b52d..31cbc8e25f 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Context.Named.Declaration
 
 let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body)
@@ -28,12 +29,14 @@ let start_deriving f suchthat lemma =
   (* spiwack: I don't know what the rigidity flag does, picked the one
      that looked the most general. *)
   let (sigma,f_type_sort) = Evd.new_sort_variable Evd.univ_flexible_alg sigma in
-  let f_type_type = Term.mkSort f_type_sort in
+  let f_type_type = EConstr.mkSort f_type_sort in
   (** create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *)
   let goals =
     let open Proofview in
         TCons ( env , sigma , f_type_type , (fun sigma f_type ->
         TCons ( env , sigma , f_type , (fun sigma ef ->
+        let f_type = EConstr.Unsafe.to_constr f_type in
+        let ef = EConstr.Unsafe.to_constr ef in
         let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in
         let evdref = ref sigma in
         let suchthat = Constrintern.interp_type_evars env' evdref suchthat in
@@ -51,9 +54,9 @@ let start_deriving f suchthat lemma =
           [suchthat], respectively. *)
       let (opaque,f_def,lemma_def) =
         match com with
-        | Admitted _ -> CErrors.error"Admitted isn't supported in Derive."
+        | Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.")
         | Proved (_,Some _,_) ->
-            CErrors.error"Cannot save a proof of Derive with an explicit name."
+            CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.")
         | Proved (opaque, None, obj) ->
             match Proof_global.(obj.entries) with
             | [_;f_def;lemma_def] ->
diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli
index 9ea876f131..3a7e7b837d 100644
--- a/plugins/derive/derive.mli
+++ b/plugins/derive/derive.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+
 (** [start_deriving f suchthat lemma] starts a proof of [suchthat]
     (which can contain references to [f]) in the context extended by
     [f:=?x]. When the proof ends, [f] is defined as the value of [?x]
diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4
index d4dc7e0eed..445923e01b 100644
--- a/plugins/derive/g_derive.ml4
+++ b/plugins/derive/g_derive.ml4
@@ -6,7 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Constrarg
+open API
+open Stdarg
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)