diff options
| author |  vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-09-28 09:59:12 +0000 |
|---|---|---|
| committer | vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-09-28 09:59:12 +0000 |
| commit | 104471118454580c3ca4b2a3cce52a03263e5d15 (patch) | |
| tree | 0af98148e169638789c3d97f3c38ecef73492a24 /parsing/g_vernac.ml4 | |
| 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/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index c61dfbf63..b7cde536f 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; |