]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/cicNotationParser.mli
notation_id were compared using Pervasives.equal this was rarely triggering the
[helm.git] / helm / software / components / content_pres / cicNotationParser.mli
index 0df3f83d06ad9f9ddc64a21b4a695f99f928652e..a348d9088bc1861816f03e0bd3ca17084efb2feb 100644 (file)
@@ -42,6 +42,8 @@ val parse_level2_meta: Ulexing.lexbuf -> CicNotationPt.term
 
 type rule_id
 
+val compare_rule_id : rule_id -> rule_id -> int
+
 val check_l1_pattern: (* level1_pattern *)
  CicNotationPt.term -> int -> Gramext.g_assoc -> checked_l1_pattern