From deadb6055aeca7a2ed944deabb96a5d9ebdbd114 Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 17 Nov 2004 15:10:26 +0000
Subject: bug module M:=N avec vm

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6321 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/cbytegen.ml    | 2 +-
 kernel/cbytegen.mli   | 4 ++--
 kernel/modops.ml      | 4 +++-
 kernel/term_typing.ml | 2 +-
 4 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 022f913ba0..108dadbb78 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -471,7 +471,7 @@ let compile env c =
   init_code,!fun_code, Array.of_list fv
 
 
-let compile_constant_body env kn body opaque boxed =
+let compile_constant_body env body opaque boxed =
   if opaque then BCconstant
   else match body with
   | None -> BCconstant
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index 407edea442..0e7434e532 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -11,6 +11,6 @@ val compile : env -> constr -> bytecodes * bytecodes * fv
                               (* init, fun, fv *)
 
 val compile_constant_body : 
-    env -> constant -> constr_substituted option -> bool -> bool -> body_code
-                                              (* opaque *) (* boxed *)
+    env -> constr_substituted option -> bool -> bool -> body_code
+                                  (* opaque *) (* boxed *)
 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 9aba4d5606..0a18978327 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -195,7 +195,9 @@ let strengthen_const env mp l cb =
       let const_subs = Some (Declarations.from_val const) in
 	{cb with 
       	   const_body = const_subs;
-	   const_opaque = false
+	   const_opaque = false;
+           const_body_code = Cemitcodes.from_val
+             (Cbytegen.compile_constant_body env const_subs false false)
 	}
 
 let strengthen_mind env mp l mib = match mib.mind_equiv with
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 291c409e9a..57c1710ff5 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -102,7 +102,7 @@ let build_constant_declaration env kn (body,typ,cst,op,boxed) =
 	  (global_vars_set env (Declarations.force b)) 
 	  (global_vars_set env typ)
   in
-  let tps = from_val (compile_constant_body env kn body op boxed) in
+  let tps = from_val (compile_constant_body env body op boxed) in
   let hyps = keep_hyps env ids in
     { const_hyps = hyps;
       const_body = body;
-- 
cgit v1.2.3