From eaa9c147f1801c363635a5be4e0258e0de1ab02e Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 27 Nov 2013 17:41:31 +0100
Subject: Refactoring: storing more information in the terminator closure.

We used to keep a lot of information in the global proof environment, for the end-of-proof commands to use. Now that the end commands are dumb, they are better stored in the proof-termination closure allocated by the starting command.

In this commit, we remove the compute_guard parameter.
---
 plugins/funind/indfun_common.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index db4297b37d..604d7d853b 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -166,7 +166,7 @@ let save with_clean id const (locality,kind) hook =
 
 
 let cook_proof _ =
-  let (id,(entry,_,strength,hook)) = Pfedit.cook_proof (fun _ -> ()) in
+  let (id,(entry,strength,hook)) = Pfedit.cook_proof (fun _ -> ()) in
   (id,(entry,strength,hook))
 
 let get_proof_clean do_reduce =
-- 
cgit v1.2.3