diff options
| author | msozeau | 2008-11-10 11:15:41 +0000 |
|---|---|---|
| committer | msozeau | 2008-11-10 11:15:41 +0000 |
| commit | fa914a0fab970de22aa1382cb7b44c6acc9b0814 (patch) | |
| tree | eec5a8cee5ae2abad91b787d4e5041c57e9b56ad /parsing | |
| parent | 51556c4088c51ab027382c773bcbac99a5394328 (diff) | |
Fix mixup between Record, Structure and Class by adding a new variant for
the three cases.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11572 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 12 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 2 |
2 files changed, 8 insertions, 6 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b48548f98a..d870c85eb0 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -220,7 +220,9 @@ GEXTEND Gram | "CoInductive" -> false ] ] ; record_token: - [ [ IDENT "Record" -> (true,true) | IDENT "Structure" -> (false,true) ]] + [ [ IDENT "Record" -> (Record,true) + | IDENT "Structure" -> (Structure,true) + | IDENT "Class" -> (Class,true) ] ] ; (* Simple definitions *) def_body: @@ -254,8 +256,8 @@ GEXTEND Gram Constructors ((c id)::l) | id = identref ; c = constructor_type -> Constructors [ c id ] | cstr = identref; "{"; fs = LIST0 record_field SEP ";"; "}" -> - RecordDecl (false,Some cstr,fs) - | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (false,None,fs) + RecordDecl (Record,Some cstr,fs) + | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (Record,None,fs) | -> Constructors [] ] ] ; (* @@ -503,7 +505,7 @@ GEXTEND Gram | IDENT "Class"; qid = identref; pars = binders_let; s = OPT [ ":"; c = lconstr -> c ]; fs = class_fields -> - VernacInductive (false, [((qid,pars,s,RecordDecl (false,None,fs)),None)]) + VernacInductive (false, [((qid,pars,s,RecordDecl (Class,None,fs)),None)]) (* Type classes *) | IDENT "Class"; sup = OPT [ l = binders_let; "=>" -> l ]; @@ -511,7 +513,7 @@ GEXTEND Gram s = OPT [ ":"; c = lconstr -> c ]; fs = class_fields -> VernacInductive - (false, [((qid,Option.cata (fun x -> x) [] sup @ pars,s,RecordDecl (false,None,fs)),None)]) + (false, [((qid,Option.cata (fun x -> x) [] sup @ pars,s,RecordDecl (Class,None,fs)),None)]) | IDENT "Context"; c = binders_let -> VernacContext c diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index e16b4e533e..0fc28d35fa 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -667,7 +667,7 @@ let rec pr_vernac = function (* Gallina extensions *) | VernacRecord ((b,coind),(oc,name),ps,s,c,fs) -> hov 2 - (str (if b then "Record" else "Class") ++ + (str (match b with Record -> "Record" | Structure -> "Structure" | Class -> "Class") ++ (if oc then str" > " else str" ") ++ pr_lident name ++ pr_and_type_binders_arg ps ++ str" :" ++ spc() ++ Option.cata pr_lconstr_expr (mt()) s ++ str" := " ++ pr_record_decl b c fs) |