diff options
| author | vsiles | 2007-09-28 09:59:12 +0000 |
|---|---|---|
| committer | vsiles | 2007-09-28 09:59:12 +0000 |
| commit | 104471118454580c3ca4b2a3cce52a03263e5d15 (patch) | |
| tree | 0af98148e169638789c3d97f3c38ecef73492a24 /parsing | |
| parent | 3d0f2b7ecfb78308bbb17d135fcceefd121f7624 (diff) | |
Modification of the Scheme command.
Now you can forget to provide the name of the scheme, it will be
built automatically depending of the sorts involved.
e.g. Scheme Induction for nat Sort Set.
will build nat_rec
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10148 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 3 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 12 |
2 files changed, 11 insertions, 4 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index c61dfbf63d..b7cde536f7 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -285,7 +285,8 @@ GEXTEND Gram ; (* Inductive schemes *) scheme: - [ [ id = identref; ":="; kind = scheme_kind -> (id,kind) ] ] + [ [ kind = scheme_kind -> (None,kind) + | id = identref; ":="; kind = scheme_kind -> (Some id,kind) ] ] ; scheme_kind: [ [ IDENT "Induction"; "for"; ind = global; diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index d44e225b50..4bb7d27520 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -279,15 +279,21 @@ let pr_binders_arg = let pr_and_type_binders_arg bl = pr_binders_arg bl -let pr_onescheme (id,schem) = +let pr_onescheme (idop,schem) = match schem with | InductionScheme (dep,ind,s) -> - hov 0 (pr_lident id ++ str" :=") ++ spc() ++ + (match idop with + | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() + | None -> spc () + ) ++ hov 0 ((if dep then str"Induction for" else str"Minimality for") ++ spc() ++ pr_reference ind) ++ spc() ++ hov 0 (str"Sort" ++ spc() ++ pr_rawsort s) | EqualityScheme ind -> - hov 0 (pr_lident id ++ str" :=") ++ spc() ++ + (match idop with + | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() + | None -> spc() + ) ++ hov 0 (str"Equality for") ++ spc() ++ pr_reference ind |