+type pattern_kind = Variable | Constructor
+type tag_t = int
+
+module type PATTERN =
+sig
+ type pattern_t
+ type term_t
+ val classify : pattern_t -> pattern_kind
+ val tag_of_pattern : pattern_t -> tag_t * pattern_t list
+ val tag_of_term : term_t -> tag_t * term_t list
+end
+
+module Matcher (P: PATTERN) :
+sig
+ val compiler:
+ (P.pattern_t * int) list ->
+ ((P.pattern_t list * int) list -> P.term_t list -> 'a) ->
+ (unit -> 'a) ->
+ (P.term_t -> 'a)
+end
+
+module Matcher21:
+sig
+ val compiler :
+ (CicNotationPt.term * int) list ->