diff options
| author | Hugo Herbelin | 2019-11-12 09:32:06 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-11-19 20:45:22 +0100 |
| commit | e7b29adca3c2ff636ff277dab843d517894f3bf6 (patch) | |
| tree | bad5adadc9fd93f6bfdd1c826538162478486713 /parsing | |
| parent | d10e7cc978a2abd97377c6365cc5366cf5cdf5eb (diff) | |
Grammar: mini-factorization between fix/cofix and Fixpoint/CoFixpoint.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.mlg | 2 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 1 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 1 |
3 files changed, 3 insertions, 1 deletions
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index bd4ce3c5ab..b9432e3247 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -130,7 +130,7 @@ GRAMMAR EXTEND Gram universe_level universe_name sort sort_family global constr_pattern lconstr_pattern Constr.ident closed_binder open_binders binder binders binders_fixannot - record_declaration typeclass_constraint pattern appl_arg; + record_declaration typeclass_constraint pattern appl_arg type_cstr; Constr.ident: [ [ id = Prim.ident -> { id } ] ] ; diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 0a41bba8ce..734dd8ee8a 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -451,6 +451,7 @@ module Constr = let typeclass_constraint = Entry.create "constr:typeclass_constraint" let record_declaration = Entry.create "constr:record_declaration" let appl_arg = Entry.create "constr:appl_arg" + let type_cstr = Entry.create "constr:type_cstr" end module Module = diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index ca5adf8ab3..404fbdb4fd 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -197,6 +197,7 @@ module Constr : 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 + val type_cstr : constr_expr Entry.t end module Module : |