X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=c9e453cf20d6c0b69fd6870b635d27eb29c93c84;hb=ccf5878f2a2ec7f952f140e162391708a740517b;hp=487bceb871377cfb1964e94ad81cccf878e8d733;hpb=37b52567b8aa1bf5807767d94b96594c0e640588;p=helm.git

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 487bceb87..c9e453cf2 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -332,10 +332,7 @@ let interpretate_term_and_interpretate_term_option
         with NRef.IllFormedReference _ ->
          CicNotationPt.fail loc "Ill formed reference")
     | CicNotationPt.NRef nref -> NCic.Const nref
-    | CicNotationPt.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
+    | CicNotationPt.NCic t -> t
     | CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector
     | CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term
     | CicNotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)