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

4 files changed, 13 insertions, 12 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index f73fe5e9cf..f0a9792fd5 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -161,7 +161,7 @@ let syntax_definition ident c local onlyparse =
 let assumption_message id =
   if_verbose message ((string_of_id id) ^ " is assumed")
 
-let declare_one_assumption is_coe (local,kind) c (_,ident) =
+let declare_one_assumption is_coe (local,kind) c nl (_,ident) =
   let r = match local with
     | Local when Lib.sections_are_opened () ->
         let _ = 
@@ -174,7 +174,7 @@ let declare_one_assumption is_coe (local,kind) c (_,ident) =
         VarRef ident
     | (Global|Local) ->
         let kn =
-          declare_constant ident (ParameterEntry c, IsAssumption kind) in
+          declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in
         assumption_message ident;
         if local=Local & Options.is_verbose () then
           msg_warning (pr_id ident ++ str" is declared as a parameter" ++
@@ -182,11 +182,11 @@ let declare_one_assumption is_coe (local,kind) c (_,ident) =
         ConstRef kn in
   if is_coe then Class.try_add_new_coercion r local
 
-let declare_assumption idl is_coe k bl c =
+let declare_assumption idl is_coe k bl c nl=
   if not (Pfedit.refining ()) then 
     let c = generalize_constr_expr c bl in
     let c = interp_type Evd.empty (Global.env()) c in
-      List.iter (declare_one_assumption is_coe k c) idl
+      List.iter (declare_one_assumption is_coe k c nl) idl
   else
     errorlabstrm "Command.Assumption"
 	(str "Cannot declare an assumption while in proof editing mode.")
@@ -799,7 +799,7 @@ let admit () =
     error "Only statements declared as conjecture can be admitted";
 *)
   let kn =
-    declare_constant id (ParameterEntry typ, IsAssumption Conjectural) in
+    declare_constant id (ParameterEntry (typ,false), IsAssumption Conjectural) in
   Pfedit.delete_current_proof ();
   assumption_message id;
   hook Global (ConstRef kn)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 4fae328056..cf05f691bf 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -36,11 +36,12 @@ val declare_definition : identifier -> definition_kind ->
 
 val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit
 
-val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types -> 
-  Names.variable located -> unit
+val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types -> bool
+  -> Names.variable located  -> unit
 
 val declare_assumption : identifier located list ->
-  coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> unit
+  coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> bool 
+  ->unit
 
 val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7dacbeabac..4c0fb5046f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -348,8 +348,8 @@ let vernac_exact_proof c =
       errorlabstrm "Vernacentries.ExactProof"
 	(str "Command 'Proof ...' can only be used at the beginning of the proof")
   	
-let vernac_assumption kind l =
-  List.iter (fun (is_coe,(idl,c)) -> declare_assumption idl is_coe kind [] c) l
+let vernac_assumption kind l nl=
+  List.iter (fun (is_coe,(idl,c)) -> declare_assumption idl is_coe kind [] c nl) l
 
 let vernac_inductive f indl = build_mutual indl f
 
@@ -1134,7 +1134,7 @@ let interp c = match c with
       vernac_start_proof k (Some id) t top f
   | VernacEndProof e -> vernac_end_proof e
   | VernacExactProof c -> vernac_exact_proof c
-  | VernacAssumption (stre,l) -> vernac_assumption stre l
+  | VernacAssumption (stre,nl,l) -> vernac_assumption stre l nl
   | VernacInductive (finite,l) -> vernac_inductive finite l
   | VernacFixpoint (l,b) -> vernac_fixpoint l b
   | VernacCoFixpoint (l,b) -> vernac_cofixpoint l b
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index cd0fb899ca..042ef1e859 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -194,7 +194,7 @@ type vernac_expr =
       (local_binder list * constr_expr) * bool * declaration_hook
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
-  | VernacAssumption of assumption_kind * simple_binder with_coercion list
+  | VernacAssumption of assumption_kind * bool * simple_binder with_coercion list
   | VernacInductive of inductive_flag * (inductive_expr * decl_notation) list
   | VernacFixpoint of (fixpoint_expr * decl_notation) list * bool
   | VernacCoFixpoint of (cofixpoint_expr * decl_notation) list * bool