From 7dc04f0244aeb277b62070f87590cbc2cafd8396 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 24 Feb 2019 20:27:09 +0100
Subject: [proof] drop parameter from terminator type

This makes the type of terminator simpler, progressing towards its
total reification.
---
 plugins/derive/derive.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index f8b5f455d1..0f0bec0129 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
@@ -99,7 +99,7 @@ let start_deriving f suchthat name : Lemmas.t =
       ignore (Declare.declare_constant name lemma_def)
   in
 
-  let terminator ?hook _ = Lemmas.Internal.make_terminator terminator in
+  let terminator = Lemmas.Internal.make_terminator terminator in
   let lemma = Lemmas.start_dependent_lemma name kind goals ~terminator in
   Lemmas.pf_map (Proof_global.map_proof begin fun p ->
     Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
-- 
cgit v1.2.3