New keyword "Inline" for Parameters and Axioms for automatic

delta-reduction at fonctor application.
Example:

Module Type S.
 Parameter Inline N : Set.
End S.

Module F (X:S).
 Definition t := X.N.
End F.

Module M.
 Definition N := nat.
End M.

Module G := F M.

Print G.t.
G.t = nat
     : Set




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9795 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 40 insertions, 19 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 7751e5bf6..e9200cd75 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -131,4 +131,4 @@ let cook_constant env r =
 	let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
 	Typeops.make_polymorphic_if_arity env typ in
   let boxed = Cemitcodes.is_boxed cb.const_body_code in
-  (body, typ, cb.const_constraints, cb.const_opaque, boxed)
+  (body, typ, cb.const_constraints, cb.const_opaque, boxed,false)
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 0646b1c22..4afdaa55e 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -25,7 +25,8 @@ type recipe = {
 
 val cook_constant :
   env -> recipe -> 
-    constr_substituted option * constant_type * constraints * bool * bool
+    constr_substituted option * constant_type * constraints * bool * bool 
+  * bool
 
 (*s Utility functions used in module [Discharge]. *)
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index d0f2289dc..1be251a50 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -49,7 +49,8 @@ type constant_body = {
     const_body_code : Cemitcodes.to_patch_substituted;
    (* const_type_code : Cemitcodes.to_patch; *)
     const_constraints : constraints;
-    const_opaque : bool }
+    const_opaque : bool; 
+    const_inline : bool}
 
 (*s Inductive types (internal representation with redundant
     information). *)
@@ -202,7 +203,8 @@ let subst_const_body sub cb = {
     const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
     (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*)
     const_constraints = cb.const_constraints;
-    const_opaque = cb.const_opaque } 
+    const_opaque = cb.const_opaque;
+    const_inline = cb.const_inline} 
 
 let subst_arity sub = function
 | Monomorphic s ->
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 22cfd62a0..7f7f7dcc3 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -47,7 +47,8 @@ type constant_body = {
     const_body_code : to_patch_substituted;
    (*i const_type_code : to_patch;i*)
     const_constraints : constraints;
-    const_opaque : bool }
+    const_opaque : bool;
+    const_inline : bool}
 
 val subst_const_body : substitution -> constant_body -> constant_body
 
diff --git a/kernel/entries.ml b/kernel/entries.ml
index fb134b1c7..17da967c2 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -62,7 +62,7 @@ type definition_entry = {
   const_entry_opaque : bool;
   const_entry_boxed  : bool}
 
-type parameter_entry = types
+type parameter_entry = types*bool
 
 type constant_entry = 
   | DefinitionEntry of definition_entry
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 61c0b8c3b..56ea852da 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -61,7 +61,7 @@ type definition_entry = {
   const_entry_opaque : bool;
   const_entry_boxed  : bool }
 
-type parameter_entry = types
+type parameter_entry = types*bool  (*inline flag*)
 
 type constant_entry = 
   | DefinitionEntry of definition_entry
diff --git a/kernel/modops.ml b/kernel/modops.ml
index e9e1d67eb..96d19552a 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -235,13 +235,29 @@ and constants_of_modtype env mp modtype =
   | MTBfunsig _ -> []
 
 (* 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,_) -> con,None) constants in 
- Mod_subst.make_resolver resolve
-
+ 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_inline then
+              let constant = lookup_constant con' env in
+		if constant.Declarations.const_opaque then
+		  None
+		else
+		  option_map Declarations.force
+		    constant.Declarations.const_body
+	    else
+              None
+	  with Not_found -> error_no_such_label (con_label con')
+	in
+	  con,constr
+     ) constants
+ in
+   Mod_subst.make_resolver resolve
 
 let strengthen_const env mp l cb = 
   match cb.const_opaque, cb.const_body with
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 8b0f45ac9..aedc44ac8 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -93,11 +93,11 @@ let infer_declaration env dcl =
       let (j,cst) = infer env c.const_entry_body in
       let (typ,cst) = constrain_type env j cst c.const_entry_type in
       Some (Declarations.from_val j.uj_val), typ, cst,
-        c.const_entry_opaque, c.const_entry_boxed
-  | ParameterEntry t ->
+        c.const_entry_opaque, c.const_entry_boxed, false
+  | ParameterEntry (t,nl) ->
       let (j,cst) = infer env t in
       None, NonPolymorphicType (Typeops.assumption_of_judgment env j), cst,
-        false, false
+        false, false, nl
 
 let global_vars_set_constant_type env = function
   | NonPolymorphicType t -> global_vars_set env t
@@ -107,7 +107,7 @@ let global_vars_set_constant_type env = function
 	  (fun t c -> Idset.union (global_vars_set env t) c))
       ctx ~init:Idset.empty
 
-let build_constant_declaration env kn (body,typ,cst,op,boxed) =
+let build_constant_declaration env kn (body,typ,cst,op,boxed,inline) =
   let ids =
     match body with 
     | None -> global_vars_set_constant_type env typ
@@ -124,7 +124,8 @@ let build_constant_declaration env kn (body,typ,cst,op,boxed) =
       const_body_code = tps;
      (* const_type_code = to_patch env typ;*)
       const_constraints = cst;
-      const_opaque = op }
+      const_opaque = op; 
+      const_inline = inline}
 
 (*s Global and local constant declaration. *)
 
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 83434e2ec..abff3e8b7 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -26,10 +26,10 @@ val translate_local_assum : env -> types ->
   types * Univ.constraints
 
 val infer_declaration : env -> constant_entry -> 
-   constr_substituted option * constant_type * constraints * bool * bool
+   constr_substituted option * constant_type * constraints * bool * bool * bool
 
 val build_constant_declaration : env -> 'a ->
-    constr_substituted option * constant_type * constraints * bool * bool ->
+    constr_substituted option * constant_type * constraints * bool * bool * bool ->
       constant_body
 
 val translate_constant : env -> constant -> constant_entry -> constant_body