Imported Upstream version 8.6upstream/8.6

3 files changed, 10 insertions, 3 deletions

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index ce93c5a3..e39d17b5 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Context.Named.Declaration
+
 let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body)
     : Safe_typing.private_constants Entries.const_entry_body =
   Future.chain ~pure:true x begin fun ((b,ctx),fx) ->
@@ -32,7 +34,7 @@ let start_deriving f suchthat lemma =
     let open Proofview in
         TCons ( env , sigma , f_type_type , (fun sigma f_type ->
         TCons ( env , sigma , f_type , (fun sigma ef ->
-        let env' = Environ.push_named (f , (Some ef) , f_type) env 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
         TCons ( env' , !evdref , suchthat , (fun sigma _ ->
@@ -49,9 +51,9 @@ let start_deriving f suchthat lemma =
           [suchthat], respectively. *)
       let (opaque,f_def,lemma_def) =
         match com with
-        | Admitted _ -> Errors.error"Admitted isn't supported in Derive."
+        | Admitted _ -> CErrors.error"Admitted isn't supported in Derive."
         | Proved (_,Some _,_) ->
-            Errors.error"Cannot save a proof of Derive with an explicit name."
+            CErrors.error"Cannot save a proof of Derive with an explicit name."
         | Proved (opaque, None, obj) ->
             match Proof_global.(obj.entries) with
             | [_;f_def;lemma_def] ->
@@ -93,6 +95,7 @@ let start_deriving f suchthat lemma =
       ignore (Declare.declare_constant lemma lemma_def)
       in
 
+  let terminator = Proof_global.make_terminator terminator in
   let () = Proof_global.start_dependent_proof lemma kind goals terminator in
   let _ = Proof_global.with_current_proof begin fun _ p ->
     Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
diff --git a/plugins/derive/derive_plugin.mllib b/plugins/derive/derive_plugin.mlpack
index 5ee0fc6d..5ee0fc6d 100644
--- a/plugins/derive/derive_plugin.mllib
+++ b/plugins/derive/derive_plugin.mlpack
diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4
index 18570a68..d4dc7e0e 100644
--- a/plugins/derive/g_derive.ml4
+++ b/plugins/derive/g_derive.ml4
@@ -6,8 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Constrarg
+
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
+DECLARE PLUGIN "derive_plugin"
+
 let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater)
 
 VERNAC COMMAND EXTEND Derive CLASSIFIED BY classify_derive_command