diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 16 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 9 |
2 files changed, 13 insertions, 12 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index ff6d998e21..03b1466481 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -151,6 +151,8 @@ GEXTEND Gram (* Gallina inductive declarations *) | f = finite_token; indl = LIST1 inductive_definition SEP "with" -> + let (k,f) = f in + let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in VernacInductive (f,false,indl) | IDENT "Boxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" -> VernacFixpoint (recs,true) @@ -171,7 +173,7 @@ GEXTEND Gram cfs = [ ":="; l = constructor_list_or_record_decl -> l | -> RecordDecl (None, []) ] -> let (recf,indf) = b in - VernacInductive (indf,infer,[((oc,name),ps,s,Some recf,cfs),None]) + VernacInductive (indf,infer,[((oc,name),ps,s,recf,cfs),None]) ] ] ; typeclass_context: @@ -214,16 +216,16 @@ GEXTEND Gram [ ["Inline" -> true | -> false] ] ; finite_token: - [ [ "Inductive" -> true - | "CoInductive" -> false ] ] + [ [ "Inductive" -> (Inductive_kw,Finite) + | "CoInductive" -> (CoInductive,CoFinite) ] ] ; infer_token: [ [ "Infer" -> true | -> false ] ] ; record_token: - [ [ IDENT "Record" -> (Record,true) - | IDENT "Structure" -> (Structure,true) - | IDENT "Class" -> (Class true,true) ] ] + [ [ IDENT "Record" -> (Record,BiFinite) + | IDENT "Structure" -> (Structure,BiFinite) + | IDENT "Class" -> (Class true,BiFinite) ] ] ; (* Simple definitions *) def_body: @@ -249,7 +251,7 @@ GEXTEND Gram [ [ id = identref; oc = opt_coercion; indpar = binders_let; c = OPT [ ":"; c = lconstr -> c ]; ":="; lc = constructor_list_or_record_decl; ntn = decl_notation -> - (((oc,id),indpar,c,None,lc),ntn) ] ] + (((oc,id),indpar,c,lc),ntn) ] ] ; constructor_list_or_record_decl: [ [ "|"; l = LIST1 constructor SEP "|" -> Constructors l diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 496af5b6e7..7b3491de22 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -594,10 +594,9 @@ let rec pr_vernac = function pr_record_decl b c fs in let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) = let kw = - match k with - | None -> str key - | Some b -> str (match b with Record -> "Record" | Structure -> "Structure" - | Class b -> if b then "Definitional Class" else "Class") + str (match k with Record -> "Record" | Structure -> "Structure" + | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" + | Class b -> if b then "Definitional Class" else "Class") in hov 0 ( kw ++ spc() ++ @@ -608,7 +607,7 @@ let rec pr_vernac = function str" :=") ++ pr_constructor_list k lc ++ pr_decl_notation pr_constr ntn in - hov 1 (pr_oneind (if f then "Inductive" else "CoInductive") (List.hd l)) + hov 1 (pr_oneind (if (Decl_kinds.recursivity_flag_of_kind f) then "Inductive" else "CoInductive") (List.hd l)) ++ (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) |