From 2debc4ab0b171963afff40cc3183e4e92cca9a0e Mon Sep 17 00:00:00 2001
From: msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 22 Jul 2008 14:02:22 +0000
Subject: Correct implementation of discharging of implicit arguments and add
 new setting "Set Manual Implicit Arguments" for manual-only implicits. Fix
 test-suite script. This removes the discharge_info argument of "dynamic"
 object's rebuild function.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11242 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/heads.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library/heads.ml')

diff --git a/library/heads.ml b/library/heads.ml
index ca1f1014f..1b1dba43f 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -158,7 +158,7 @@ let discharge_head (_,(ref,k)) =
   | EvalConstRef cst -> Some (EvalConstRef (pop_con cst), k)
   | EvalVarRef id -> None
 
-let rebuild_head (info,(ref,k)) =
+let rebuild_head (ref,k) =
   (ref, compute_head ref)
 
 let export_head o = Some o
-- 
cgit v1.2.3