diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 560a9a757..58899e607 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -354,13 +354,13 @@ GEXTEND Gram ; scheme_kind: [ [ IDENT "Induction"; "for"; ind = smart_global; - IDENT "Sort"; s = sort-> InductionScheme(true,ind,s) + IDENT "Sort"; s = sort_family-> InductionScheme(true,ind,s) | IDENT "Minimality"; "for"; ind = smart_global; - IDENT "Sort"; s = sort-> InductionScheme(false,ind,s) + IDENT "Sort"; s = sort_family-> InductionScheme(false,ind,s) | IDENT "Elimination"; "for"; ind = smart_global; - IDENT "Sort"; s = sort-> CaseScheme(true,ind,s) + IDENT "Sort"; s = sort_family-> CaseScheme(true,ind,s) | IDENT "Case"; "for"; ind = smart_global; - IDENT "Sort"; s = sort-> CaseScheme(false,ind,s) + IDENT "Sort"; s = sort_family-> CaseScheme(false,ind,s) | IDENT "Equality"; "for" ; ind = smart_global -> EqualityScheme(ind) ] ] ; (* Various Binders *) |