X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationParser.mli;h=80d79ef448e5f664bbd5153b832b5b3f934afa41;hb=f981a524748846acc29b76b6e616af110b4ee13d;hp=083d442eb15511a3b7f5ecd856828740969f9303;hpb=e20f3963028a966fc93ba0d611c4aa8341d20e2c;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationParser.mli b/helm/ocaml/cic_notation/cicNotationParser.mli index 083d442eb..80d79ef44 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.mli +++ b/helm/ocaml/cic_notation/cicNotationParser.mli @@ -40,9 +40,9 @@ val parse_level2_meta: char Stream.t -> CicNotationPt.term type rule_id val extend: - CicNotationPt.term -> - ?precedence:int -> - ?associativity:Gramext.g_assoc -> + CicNotationPt.term -> (* level 1 pattern *) + precedence:int -> + associativity:Gramext.g_assoc -> (CicNotationEnv.t -> CicNotationPt.location -> CicNotationPt.term) -> rule_id