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

1 files changed, 6 insertions, 5 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 8b0f45ac9c..aedc44ac8f 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. *)