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, 1 insertions, 1 deletions

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