diff options
| author | soubiran | 2007-04-25 15:13:45 +0000 |
|---|---|---|
| committer | soubiran | 2007-04-25 15:13:45 +0000 |
| commit | 40425048feff138e6c67555c7ee94142452d1cae (patch) | |
| tree | b26134c830f386838f219b92a1c8960dd50c4287 /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 11 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 2 |
2 files changed, 8 insertions, 5 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 34d7997456..6d0e3ffc43 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -120,11 +120,11 @@ GEXTEND Gram [ [ thm = thm_token; id = identref; bl = LIST0 binder_let; ":"; c = lconstr -> VernacStartTheoremProof (thm, id, (bl, c), false, no_hook) - | stre = assumption_token; bl = assum_list -> - VernacAssumption (stre, bl) - | stre = assumptions_token; bl = assum_list -> + | stre = assumption_token; nl = inline; bl = assum_list -> + VernacAssumption (stre, nl, bl) + | stre = assumptions_token; nl = inline; bl = assum_list -> test_plurial_form bl; - VernacAssumption (stre, bl) + VernacAssumption (stre, nl, bl) | IDENT "Boxed";"Definition";id = identref; b = def_body -> VernacDefinition ((Global,true,Definition), id, b, no_hook) | IDENT "Unboxed";"Definition";id = identref; b = def_body -> @@ -193,6 +193,9 @@ GEXTEND Gram | IDENT "Axioms" -> (Global, Logical) | IDENT "Parameters" -> (Global, Definitional) ] ] ; + inline: + [ ["Inline" -> true | -> false] ] + ; finite_token: [ [ "Inductive" -> true | "CoInductive" -> false ] ] diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 7d4104db3e..c2571ad0ae 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -515,7 +515,7 @@ let rec pr_vernac = function | Some tok -> str"Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id)) | VernacExactProof c -> hov 2 (str"Proof" ++ pr_lconstrarg c) - | VernacAssumption (stre,l) -> + | VernacAssumption (stre,_,l) -> let n = List.length (List.flatten (List.map fst (List.map snd l))) in hov 2 (pr_assumption_token (n > 1) stre ++ spc() ++ |