From 5439626efe5ed3aa4b6ac01f2116a6a8ab6a3f92 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 29 Nov 2010 13:02:02 +0000 Subject: [PATCH] Back-porting from new Matita: Invariant dropped: NotationPt.NCic t can now contain metas. We do not know if the invariant was exploited somewhere... --- .../components/ng_disambiguation/nCicDisambiguate.ml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) 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) -- 2.39.2