From 4d7c59271640be57e8ba0691c03c6f8088d625ef Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 18 Nov 2010 10:02:14 +0000 Subject: [PATCH] Invariant dropped: NotationPt.NCic t can now contain metas. We do not know if the invariant was exploited somewhere... --- matita/components/ng_disambiguation/nCicDisambiguate.ml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) 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) -- 2.39.2