We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 35988a2 commit 5cedc3cCopy full SHA for 5cedc3c
src/Parsers/BaseTypes.v
@@ -80,9 +80,12 @@ Section recursive_descent_parser.
80
: production_carrierT -> String -> nat -> nat -> list nat }.
81
82
Class boolean_parser_dataT :=
83
- { predata :> parser_computational_predataT;
84
- split_data :> split_dataT }.
85
-
+ { predata : parser_computational_predataT;
+ split_data : split_dataT }.
+ (* Use :> and remove the following lines,
86
+ once Coq 8.16 is the minimum required version. *)
87
+ #[export] Existing Instance predata.
88
+ #[export] Existing Instance split_data.
89
Global Coercion predata : boolean_parser_dataT >-> parser_computational_predataT.
90
Global Coercion split_data : boolean_parser_dataT >-> split_dataT.
91
End recursive_descent_parser.
0 commit comments