* added backtracking in matching code (hairy code!)

[helm.git] / helm / ocaml / cic_notation / cicNotationMatcher.mli

diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.mli b/helm/ocaml/cic_notation/cicNotationMatcher.mli
index 55de82999f9aa8537637a7838a0c374324570719..4abb5b8bc9b37127e77243f74172f025f38e8459 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationMatcher.mli
+++ b/helm/ocaml/cic_notation/cicNotationMatcher.mli
@@ -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: