From 8ef8ea4a7d2bd37d5d6fa55d482459881c067e85 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sat, 28 Mar 2009 20:58:42 +0000
Subject: Fix bug #2056 (discharge bug).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12029 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/recordops.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index b6749db198..16d3331aad 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -65,8 +65,11 @@ let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) =
     if projs' == projs && kn' == kn && id' == id then obj else
       ((kn',i),id',kl,projs')
 
+let discharge_constructor (ind, n) = 
+  (Lib.discharge_inductive ind, n)
+
 let discharge_structure (_,(ind,id,kl,projs)) =
-  Some (Lib.discharge_inductive ind, id, kl,
+  Some (Lib.discharge_inductive ind, discharge_constructor id, kl,
         List.map (Option.map Lib.discharge_con) projs)
 
 let (inStruc,outStruc) =
-- 
cgit v1.2.3