- new syntax for let rec/corec with flavor specifier (tested on lambdadelta/ground_2/)

[helm.git] / matita / components / ng_disambiguation / grafiteDisambiguate.ml

diff --git a/matita/components/ng_disambiguation/grafiteDisambiguate.ml b/matita/components/ng_disambiguation/grafiteDisambiguate.ml
index baa28b2d62c362a964d8a324f456197798b5a9ee..9cfbbc8c0a184b75a47a68d7a2d3ab12b6b49c34 100644 (file)
--- 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 _