Matita 0.99.* bug fixed: new alias insertion

[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 dbdd2131304c1ec34b4da5a0e717fa24e7743ab9..7b1e2c50869f4e5b93fbc112f3b116515d58825a 100644 (file)
--- a/matita/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matita/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -57,9 +57,9 @@ class virtual status =
 let eval_with_new_aliases status f =
  let status =
   status#set_disambiguate_db { status#disambiguate_db with new_aliases = [] } in
- let res = f status in
- let new_aliases = status#disambiguate_db.new_aliases in
-  new_aliases,res
+ let new_status = f status in
+ let new_aliases = new_status#disambiguate_db.new_aliases in
+  new_aliases,new_status
 ;;
 
 let dump_aliases out msg status =
@@ -248,9 +248,11 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj) =
    in
    let name = 
      match obj with
-     | NotationPt.Inductive (_,(name,_,_,_)::_)
-     | NotationPt.Record (_,name,_,_) -> name ^ ".ind"
-     | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
+     | 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)