diff options
| author | vsiles | 2007-05-25 14:47:02 +0000 |
|---|---|---|
| committer | vsiles | 2007-05-25 14:47:02 +0000 |
| commit | 46dcebf37f85781cc7f622f1bec7314bc6af26d5 (patch) | |
| tree | b2d2fb246e0a2b3dbf932ca7409ccbc0646a8890 /parsing | |
| parent | db50dfc5e752f7209c10256d8af86f24677221d1 (diff) | |
Modification of VernacScheme to handle a new scheme: Equality (equality in
boolean, will be added later) and update so everything is fine with the new
syntax.
New Type:
type scheme =
| InductionScheme of bool * lreference * sort_expr
| EqualityScheme of lreference
...
| VernacScheme of (lident * scheme) list
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9860 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 15 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 16 |
2 files changed, 19 insertions, 12 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 73e366c931..94e39621e9 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -280,13 +280,14 @@ GEXTEND Gram ; (* Inductive schemes *) scheme: - [ [ id = identref; ":="; dep = dep_scheme; "for"; ind = global; - IDENT "Sort"; s = sort -> - (id,dep,ind,s) ] ] - ; - dep_scheme: - [ [ IDENT "Induction" -> true - | IDENT "Minimality" -> false ] ] + [ [ id = identref; ":="; kind = scheme_kind -> (id,kind) ] ] + ; + scheme_kind: + [ [ IDENT "Induction"; "for"; ind = global; + IDENT "Sort"; s = sort-> InductionScheme(true,ind,s) + | IDENT "Minimality"; "for"; ind = global; + IDENT "Sort"; s = sort-> InductionScheme(false,ind,s) + | IDENT "Equality"; "for" ; ind = global -> EqualityScheme(ind) ] ] ; (* Various Binders *) (* diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 62af97b439..f12f730610 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -279,11 +279,17 @@ let pr_binders_arg = let pr_and_type_binders_arg bl = pr_binders_arg bl -let pr_onescheme (id,dep,ind,s) = - hov 0 (pr_lident id ++ str" :=") ++ 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) +let pr_onescheme (id,schem) = + match schem with + | InductionScheme (dep,ind,s) -> + hov 0 (pr_lident id ++ str" :=") ++ 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() ++ + hov 0 (str"Equality for") + ++ spc() ++ pr_reference ind let begin_of_inductive = function [] -> 0 |