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.
---
 vernac/declareObl.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'vernac/declareObl.ml')

diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 564e83efd5..2afd056950 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -486,13 +486,13 @@ let dependencies obls n =
     obls;
   !res
 
-let obligation_terminator name num guard auto pf =
+let obligation_terminator name num auto pf =
   let open Proof_global in
   let open Lemmas in
-  let term = standard_proof_terminator guard in
+  let term = Lemmas.standard_proof_terminator in
   match pf with
   | Admitted _ -> Internal.apply_terminator term pf
-  | Proved (opq, id, { entries=[entry]; universes=uctx }, hook ) -> begin
+  | Proved (opq, id, { entries=[entry]; universes=uctx }, hook, compute_guard ) -> begin
     let env = Global.env () in
     let ty = entry.Entries.const_entry_type in
     let body, eff = Future.force entry.const_entry_body in
@@ -552,5 +552,5 @@ let obligation_terminator name num guard auto pf =
       let e = CErrors.push e in
       pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))
   end
-  | Proved (_, _, _,_ ) ->
+  | Proved (_, _, _,_,_) ->
     CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term")
-- 
cgit v1.2.3