]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationMatcher.mli
snapshot, notably:
[helm.git] / helm / ocaml / cic_notation / cicNotationMatcher.mli
index 55de82999f9aa8537637a7838a0c374324570719..3846bf52857f43c49f1fba9ae6f7763d21317968 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:
@@ -54,6 +54,7 @@ end
 module Matcher32:
 sig
   val compiler :
-    (CicNotationPt.cic_appl_pattern * int) list ->
+    (GrafiteAst.cic_appl_pattern * int) list ->
       (Cic.annterm -> ((string * Cic.annterm) list * int) option)
 end
+