new syntax

[helm.git] / helm / software / matita / matitaTypes.mli

diff --git a/helm/software/matita/matitaTypes.mli b/helm/software/matita/matitaTypes.mli
index 34e98cc1ad112899f5d8452798a3f4832f84490e..ecc78a629085d54df4c3325cb90930d84c37c36c 100644 (file)
--- a/helm/software/matita/matitaTypes.mli
+++ b/helm/software/matita/matitaTypes.mli
@@ -32,6 +32,7 @@ type mathViewer_entry =
   [ `About of abouts
   | `Check of string
   | `Cic of Cic.term * Cic.metasenv
+  | `NCic of NCic.term * NCic.context * NCic.metasenv * NCic.substitution
   | `Dir of string
   | `HBugs of [ `Tutors ]
   | `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ]