support for terms with metas in check

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

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index 1db5bb0de04ea2efb8454458d3da9b73d00f8478..26299967224cb6b4f850da5a53935360691296e9 100644 (file)
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -198,7 +198,7 @@ class type interpreter =
 
 type term_source =
   [ `Ast of DisambiguateTypes.term
-  | `Cic of Cic.term
+  | `Cic of Cic.term * Cic.metasenv
   | `String of string
   ]