From 2100f292ee109f9a75eb9d79c2234846d7135755 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Wed, 23 Apr 2008 11:51:44 +0000
Subject: correction du bug sur Parameter Inline que j'ai reouvert hier par
 inadvertance

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10837 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/modops.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'kernel')

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 0d0af00f09..590db27274 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -263,11 +263,11 @@ let rec eval_struct env = function
 	      (subst_key (map_msid msid mp) sub_alias)
 	      (map_msid msid mp)
 	| _ -> sub_alias in
-      let sub_alias = update_subst_alias sub_alias 
+      let sub_alias1 = update_subst_alias sub_alias 
 	(map_mbid farg_id mp (None)) in
       let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in
 	eval_struct env (subst_struct_expr 
-			   (join sub_alias 
+			   (join sub_alias1 
 			      (map_mbid farg_id mp (Some resolve))) fbody_b)
   | SEBwith (mtb,(With_definition_body _ as wdb)) ->
       let mtb',_ = merge_with env mtb wdb empty_subst in
@@ -437,8 +437,9 @@ and  resolver_of_environment mbid modtype mp alias env =
  let rec make_resolve = function
    | [] -> []
    | (con,expecteddef)::r ->
-       let con',_ = subst_con alias con in
-       let con' = replace_mp_in_con (MPbound mbid) mp con' in
+       let con' = replace_mp_in_con (MPbound mbid) mp con in
+       let con',_ = subst_con alias con' in
+  (*     let con' = replace_mp_in_con (MPbound mbid) mp con' in *)
 	 try
 	   if expecteddef.Declarations.const_inline then
 	     let constant = lookup_constant con' env in
-- 
cgit v1.2.3