support for terms with metas in check

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

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 73a5da1a1c3bc863df34b0516c9724e0b709c09e..95618d142624e932493666da151773b8d9f412c5 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -160,7 +160,7 @@ class type interpreter =
 
 type term_source =
   [ `Ast of DisambiguateTypes.term
-  | `Cic of Cic.term
+  | `Cic of Cic.term * Cic.metasenv
   | `String of string
   ]