X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=be5aacb93b1daf512730eed4ab846b58c8b5680c;hb=d78c800805af2b4b7718a8af9b533592b88cd6ea;hp=cdb90ea0212761a4d7e0e31870fe7606719998d4;hpb=f6b7c6ae353e014761a3d24dbc87e00d828d7f2d;p=helm.git

diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml
index cdb90ea02..be5aacb93 100644
--- a/matita/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml
@@ -328,10 +328,7 @@ let interpretate_term_and_interpretate_term_option
         with NRef.IllFormedReference _ ->
          NotationPt.fail loc "Ill formed reference")
     | NotationPt.NRef nref -> NCic.Const nref
-    | NotationPt.NCic t -> 
-           let context = (* to make metas_of_term happy *)
-             List.map (fun x -> x,NCic.Decl (NCic.Implicit `Type)) context in
-           assert(NCicUntrusted.metas_of_term [] context t = []); t
+    | NotationPt.NCic t ->  t
     | NotationPt.Implicit `Vector -> NCic.Implicit `Vector
     | NotationPt.Implicit `JustOne -> NCic.Implicit `Term
     | NotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)