diff options
| author |  soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-25 15:13:45 +0000 |
|---|---|---|
| committer | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-25 15:13:45 +0000 |
| commit | 40425048feff138e6c67555c7ee94142452d1cae (patch) | |
| tree | b26134c830f386838f219b92a1c8960dd50c4287 /kernel/term_typing.mli | |
| parent | 2c75beb4e24c91d3ecab07ca9279924205002ada (diff) | |
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
Diffstat (limited to 'kernel/term_typing.mli')
| -rw-r--r-- | kernel/term_typing.mli | 4 |
1 files changed, 2 insertions, 2 deletions
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 |