From 5514d654d2d8b29a46d65d0f38bdf36a69c56f45 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 30 May 2006 21:32:10 +0000
Subject: retour au comportement antérieur pour une application de foncteur:
 plus d'expansions, un foncteur F dependant de X donne une fois appliquee a M
 un module dont le corps est simplement celui de F avec des M a la place des
 X.

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

(limited to 'kernel')

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 5fece5b1fd..aacc8f30c2 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -190,35 +190,13 @@ and constants_of_modtype env mp modtype =
       (subst_signature_msid msid mp sign)
   | MTBfunsig _ -> []
 
-(* returns a resolver for kn that maps mbid to mp and then delta-expands
-   the obtained constants according to env *)
+(* returns a resolver for kn that maps mbid to mp *)
+(* Nota: Some delta-expansions used to happen here. 
+    Browse SVN if you want to know more. *)
 let resolver_of_environment mbid modtype mp env =
  let constants = constants_of_modtype env (MPbound mbid) modtype in
- let resolve =
-  List.map
-   (fun (con,expecteddef) ->
-     let con' = replace_mp_in_con (MPbound mbid) mp con in
-     let constr =
-      try
-       if expecteddef.Declarations.const_body <> None then
-        (* Do not expand constants that already have a body in the
-           expected type (i.e. only parameters/axioms in the module type
-           are expanded). In the few examples we have this seems to
-           be the more reasonable behaviour for the user. *)
-        None
-       else
-        let constant = lookup_constant con' env in
-         if constant.Declarations.const_opaque then
-          None
-         else
-          option_map Declarations.force
-           constant.Declarations.const_body
-      with Not_found -> error_no_such_label (con_label con')
-     in
-      con,constr
-   ) constants
- in
-  Mod_subst.make_resolver resolve
+ let resolve = List.map (fun (con,_) -> con,None) constants in 
+ Mod_subst.make_resolver resolve
 
 (* we assume that the substitution of "mp" into "msid" is already done
 (or unnecessary) *)
-- 
cgit v1.2.3