X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_disambiguation%2FgrafiteDisambiguate.ml;h=9cfbbc8c0a184b75a47a68d7a2d3ab12b6b49c34;hb=5832735b721c0bd8567c8f0be761a9136363a2a6;hp=baa28b2d62c362a964d8a324f456197798b5a9ee;hpb=064980eacc2efe70ffee96134d75dfa37506fc36;p=helm.git diff --git a/matita/components/ng_disambiguation/grafiteDisambiguate.ml b/matita/components/ng_disambiguation/grafiteDisambiguate.ml index baa28b2d6..9cfbbc8c0 100644 --- a/matita/components/ng_disambiguation/grafiteDisambiguate.ml +++ b/matita/components/ng_disambiguation/grafiteDisambiguate.ml @@ -248,8 +248,8 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj) = in let name = match obj with - | NotationPt.Inductive (_,(name,_,_,_)::_) - | NotationPt.Record (_,name,_,_) -> name ^ ".ind" + | NotationPt.Inductive (_,(name,_,_,_)::_,_) + | NotationPt.Record (_,name,_,_,_) -> name ^ ".ind" | NotationPt.Theorem (name,_,_,_) -> name ^ ".con" | NotationPt.LetRec (_,(_,(NotationPt.Ident (name, None),_),_,_)::_,_) -> name ^ ".con" | NotationPt.LetRec _