X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_disambiguation%2FgrafiteDisambiguate.ml;h=1f3df5bfba8c24e9d1ab479e3e4eb2299e58d0fd;hb=5ddacb0ce9c69c9bab984e1cd28fc65c617880a4;hp=dbdd2131304c1ec34b4da5a0e717fa24e7743ab9;hpb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;p=helm.git

diff --git a/matita/components/ng_disambiguation/grafiteDisambiguate.ml b/matita/components/ng_disambiguation/grafiteDisambiguate.ml
index dbdd21313..1f3df5bfb 100644
--- a/matita/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matita/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -50,16 +50,16 @@ class virtual status =
   method disambiguate_db = disambiguate_db
   method set_disambiguate_db v = {< disambiguate_db = v >}
   method set_disambiguate_status
-   : 'status. #g_status as 'status -> 'self
+   : 'status. (#g_status as 'status) -> 'self
       = fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db)
  end
 
 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 =
@@ -122,7 +122,7 @@ let ncic_mk_choice status = function
      let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
       desc, `Num_interp
        (fun num -> match f with `Num_interp f -> f num | _ -> assert false)
-  | GrafiteAst.Ident_alias (name, uri) -> 
+  | GrafiteAst.Ident_alias (_name, uri) -> 
      uri, `Sym_interp 
       (fun l->assert(l = []);
         let nref = NReference.reference_of_string uri in
@@ -139,7 +139,7 @@ let mk_implicit b =
 ;;
 
 let nlookup_in_library 
-  interactive_user_uri_choice input_or_locate_uri item 
+  _interactive_user_uri_choice _input_or_locate_uri item 
 =
   match item with
   | DisambiguateTypes.Id id -> 
@@ -206,8 +206,8 @@ let disambiguate_npattern status (text, prefix_len, (wanted, hyp_paths, goal_pat
    (wanted, hyp_paths, goal_path)
 ;;
 
-let disambiguate_reduction_kind text prefix_len = function
-  | `Unfold (Some t) -> assert false (* MATITA 1.0 *)
+let disambiguate_reduction_kind _text _prefix_len = function
+  | `Unfold (Some _t) -> assert false (* MATITA 1.0 *)
   | `Normalize
   | `Simpl
   | `Unfold None
@@ -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)