From 6a246d5d5ec12f618d241407092691595b4f733b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 19 Aug 2015 17:24:54 +0200
Subject: Opacifying the proof_terminator type.

---
 plugins/derive/derive.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/derive')

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index c232ae31a..96d5279a7 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -93,6 +93,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
-- 
cgit v1.2.3