X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=cdb90ea0212761a4d7e0e31870fe7606719998d4;hb=b108ab28153129d6578d7d9c2ffdf19e6779d86f;hp=2c5b06394d9ed7223eb12879d92f44b9955a2b8e;hpb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;p=helm.git

diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml
index 2c5b06394..cdb90ea02 100644
--- a/matita/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml
@@ -14,7 +14,6 @@
 open Printf
 
 open DisambiguateTypes
-open UriManager
 
 module Ast = NotationPt
 module NRef = NReference 
@@ -22,9 +21,6 @@ module NRef = NReference
 let debug_print s = prerr_endline (Lazy.force s);;
 let debug_print _ = ();;
 
-let reference_of_oxuri = ref (fun _ -> assert false);;
-let set_reference_of_oxuri f = reference_of_oxuri := f;;
-
 let cic_name_of_name = function
   | Ast.Ident (n, None) ->  n
   | _ -> assert false
@@ -328,7 +324,7 @@ let interpretate_term_and_interpretate_term_option
     | NotationPt.Uri (uri, subst) ->
        assert (subst = None);
        (try
-         NCic.Const (!reference_of_oxuri(UriManager.uri_of_string uri))
+         NCic.Const (NReference.reference_of_string uri)
         with NRef.IllFormedReference _ ->
          NotationPt.fail loc "Ill formed reference")
     | NotationPt.NRef nref -> NCic.Const nref
@@ -352,14 +348,10 @@ let interpretate_term_and_interpretate_term_option
     | NotationPt.Sort `Prop -> NCic.Sort NCic.Prop
     | NotationPt.Sort `Set -> NCic.Sort (NCic.Type
        [`Type,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
-    | NotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type
-       [`Type,NUri.uri_of_string "cic:/matita/pts/Type0.univ"])
     | NotationPt.Sort (`NType s) -> NCic.Sort (NCic.Type
        [`Type,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
     | NotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type
        [`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
-    | NotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type
-       [`CProp,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
     | NotationPt.Symbol (symbol, instance) ->
         Disambiguate.resolve ~env ~mk_choice 
          (Symbol (symbol, instance)) (`Args [])
@@ -414,17 +406,6 @@ let disambiguate_path path =
     ~uri:None ~is_path:true ~localization_tbl) ~context:[] path
 ;;
 
-let new_flavour_of_flavour = function 
-  | `Definition -> `Definition
-  | `MutualDefinition -> `Definition 
-  | `Fact -> `Fact
-  | `Lemma -> `Lemma
-  | `Remark -> `Example
-  | `Theorem -> `Theorem
-  | `Variant -> `Corollary 
-  | `Axiom -> `Fact
-;;
-
 let ncic_name_of_ident = function
   | Ast.Ident (name, None) -> name
   | _ -> assert false
@@ -451,11 +432,11 @@ let interpretate_obj
      uri, height, [], [], 
      (match bo,flavour with
       | None,`Axiom -> 
-          let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
+          let attrs = `Provided, flavour, pragma in
           NCic.Constant ([],name,None,ty',attrs)
       | Some _,`Axiom -> assert false
       | None,_ ->
-          let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
+          let attrs = `Provided, flavour, pragma in
           NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs)
       | Some bo,_ ->
         (match bo with
@@ -492,14 +473,14 @@ let interpretate_obj
                    ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
                  defs
              in
-             let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
+             let attrs = `Provided, flavour, pragma in
              NCic.Fixpoint (inductive,inductiveFuns,attrs)
          | bo -> 
              let bo = 
                interpretate_term 
                 ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
              in
-             let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
+             let attrs = `Provided, flavour, pragma in
              NCic.Constant ([],name,Some bo,ty',attrs)))
  | NotationPt.Inductive (params,tyl) ->
     let context,params =