attached macros: hint(partial), check

[helm.git] / helm / matita / matitaTypes.ml

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 48d419341ca4b2fad4aefbf7891c23dc4b1b868a..454c17a7f521afc53be9b9fc9460d75ba3a4b564 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -145,3 +145,14 @@ class type console =
     method show : ?msg:string -> unit -> unit
   end
 
+type term_source =
+  [ `Ast of DisambiguateTypes.term
+  | `Cic of Cic.term * Cic.metasenv
+  | `String of string
+  ]
+
+class type mathViewer =
+  object
+    method show_term: term_source -> unit
+  end
+