]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/ng_cic_content/ncic2astMatcher.mli
arithmetics for λδ
[helm.git] / matita / components / ng_cic_content / ncic2astMatcher.mli
index 1feae63b01be371cf8cc1f98d1efefe53087013f..47721cf4ee346a290dfe0149277e27cef8cac198 100644 (file)
  * http://helm.cs.unibo.it/
  *)
 
-val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit
-
 module Matcher32:
 sig
   (** @param l3_patterns level 3 (CIC) patterns (AKA cic_appl_pattern) *)
   val compiler :
+   #NCic.status ->
     (NotationPt.cic_appl_pattern * int) list ->
       (NCic.term ->
         ((string * NCic.term) list * NCic.term list * int) option)