notation ast updated to comply with the toplevel let rec of ng_kernel

[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 3601f4c443a5b94f3685bd7414c88f9f89c3d9aa..baa28b2d62c362a964d8a324f456197798b5a9ee 100644 (file)
--- a/matita/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matita/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -251,6 +251,8 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj) =
      | NotationPt.Inductive (_,(name,_,_,_)::_)
      | NotationPt.Record (_,name,_,_) -> name ^ ".ind"
      | NotationPt.Theorem (name,_,_,_) -> name ^ ".con"
+     | NotationPt.LetRec (_,(_,(NotationPt.Ident (name, None),_),_,_)::_,_) -> name ^ ".con"
+     | NotationPt.LetRec _
      | NotationPt.Inductive _ -> assert false
    in
      NUri.uri_of_string (baseuri ^ "/" ^ name)