From a2ea73d84be2fe95eeda42f5f5ac458f0af9968f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 24 Feb 2019 01:57:59 +0100
Subject: [proofs] Store hooks in the proof object.

As of now, hooks were stored in the terminators as closures, we place
them instead in the proof object and are thus passed back at proof
closing time.

This helps towards the reification and unification of terminators.
---
 plugins/derive/derive.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/derive')

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index aad3967f6d..f8b5f455d1 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -56,9 +56,9 @@ let start_deriving f suchthat name : Lemmas.t =
       let (opaque,f_def,lemma_def) =
         match com with
         | Lemmas.Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.")
-        | Lemmas.Proved (_,Some _,_) ->
+        | Lemmas.Proved (_,Some _,_, _) ->
             CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.")
-        | Lemmas.Proved (opaque, None, obj) ->
+        | Lemmas.Proved (opaque, None, obj,_) ->
             match Proof_global.(obj.entries) with
             | [_;f_def;lemma_def] ->
                 opaque <> Proof_global.Transparent , f_def , lemma_def
-- 
cgit v1.2.3