diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.mlg | 14 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 |
2 files changed, 8 insertions, 8 deletions
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 0586dda555..7786155092 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -56,10 +56,10 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) : fix_expr = (id,ann,bl,ty,body) let mk_cofixb (id,bl,ann,body,(loc,tyc)) : cofix_expr = - let _ = Option.map (fun { CAst.loc = aloc } -> + Option.iter (fun { CAst.loc = aloc } -> CErrors.user_err ?loc:aloc ~hdr:"Constr:mk_cofixb" - (Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in + (Pp.str"Annotation forbidden in cofix expression.")) ann; let ty = match tyc with Some ty -> ty | None -> CAst.make @@ CHole (None, IntroAnonymous, None) in @@ -440,10 +440,10 @@ GRAMMAR EXTEND Gram ] ] ; fixannot: - [ [ "{"; IDENT "struct"; id=identref; "}" -> { (Some id, CStructRec) } - | "{"; IDENT "wf"; rel=constr; id=OPT identref; "}" -> { (id, CWfRec rel) } + [ [ "{"; IDENT "struct"; id=identref; "}" -> { CStructRec id } + | "{"; IDENT "wf"; rel=constr; id=identref; "}" -> { CWfRec(id,rel) } | "{"; IDENT "measure"; m=constr; id=OPT identref; - rel=OPT constr; "}" -> { (id, CMeasureRec (m,rel)) } + rel=OPT constr; "}" -> { CMeasureRec (id,m,rel) } ] ] ; impl_name_head: @@ -452,9 +452,9 @@ GRAMMAR EXTEND Gram binders_fixannot: [ [ na = impl_name_head; assum = impl_ident_tail; bl = binders_fixannot -> { (assum na :: fst bl), snd bl } - | f = fixannot -> { [], f } + | f = fixannot -> { [], Some (CAst.make ~loc f) } | b = binder; bl = binders_fixannot -> { b @ fst bl, snd bl } - | -> { [], (None, CStructRec) } + | -> { [], None } ] ] ; open_binders: diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 5d8897cb47..84d19730fa 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -191,7 +191,7 @@ module Constr : val binder : local_binder_expr list Entry.t (* closed_binder or variable *) val binders : local_binder_expr list Entry.t (* list of binder *) val open_binders : local_binder_expr list Entry.t - val binders_fixannot : (local_binder_expr list * (lident option * recursion_order_expr)) Entry.t + val binders_fixannot : (local_binder_expr list * recursion_order_expr CAst.t option) Entry.t val typeclass_constraint : (lname * bool * constr_expr) Entry.t val record_declaration : constr_expr Entry.t val appl_arg : (constr_expr * explicitation CAst.t option) Entry.t |