]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationMatcher.mli
packaging cleanup: get rid of ancient debhelpers, use dh_install
[helm.git] / helm / ocaml / cic_notation / cicNotationMatcher.mli
index 55de82999f9aa8537637a7838a0c374324570719..4a9d4a27548b5e1a5e809a45915de74485148ba6 100644 (file)
@@ -39,9 +39,9 @@ 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)
+    ((P.pattern_t list * int) list -> P.term_t list -> 'a option) ->
+    (unit -> 'a option) ->
+      (P.term_t -> 'a option)
 end
 
 module Matcher21:
@@ -57,3 +57,4 @@ sig
     (CicNotationPt.cic_appl_pattern * int) list ->
       (Cic.annterm -> ((string * Cic.annterm) list * int) option)
 end
+