X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=f221a2b05a57a31596ab767c2a8438f1d40a919c;hb=204600c93b7e4d0bbd8c414835c6d57917b1f1a0;hp=d50eec79600b12358ecd7bc5af9d84f4ae7f4d47;hpb=7288b45eacf9f7dcd118b3b89b81ff19ae9d6ce5;p=helm.git

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index d50eec796..f221a2b05 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -332,6 +332,10 @@ 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.Implicit `Vector -> NCic.Implicit `Vector
     | CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term
     | CicNotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)