X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=6e72042e83c6a34901de94fe5607e6f41ecc9088;hb=6b0a195b180e3526af7b55771b2df7b10acd7c30;hp=520db6aca994a6710ba955362387803e8564d7a7;hpb=7ce251730873891f2975bc8c46b122e842d203db;p=helm.git

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 520db6aca..6e72042e8 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -312,21 +312,23 @@ let interpretate_term_and_interpretate_term_option
         NCic.LetIn (cic_name, cic_typ, cic_def, cic_body)
     | CicNotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term
     | CicNotationPt.Ident _
-    | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
+    | CicNotationPt.Uri _
+    | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
     | CicNotationPt.Ident (name, subst) ->
        assert (subst = None);
        (try
-         NCic.Rel (find_in_context name context)
+             NCic.Rel (find_in_context name context)
        with Not_found -> 
          try NCic.Const (List.assoc name obj_context)
          with Not_found ->
            Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
-    | CicNotationPt.Uri (name, subst) ->
+    | CicNotationPt.Uri (uri, subst) ->
        assert (subst = None);
        (try
-         NCic.Const (NRef.reference_of_string name)
+         NCic.Const (OCic2NCic.reference_of_oxuri(UriManager.uri_of_string uri))
         with NRef.IllFormedReference _ ->
          CicNotationPt.fail loc "Ill formed reference")
+    | CicNotationPt.NRef nref -> NCic.Const nref
     | CicNotationPt.Implicit -> NCic.Implicit `Term
     | CicNotationPt.UserInput -> NCic.Implicit `Hole
     | CicNotationPt.Num (num, i) -> 
@@ -342,11 +344,13 @@ let interpretate_term_and_interpretate_term_option
     | CicNotationPt.Sort `Set -> NCic.Sort (NCic.Type
        [false,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
     | CicNotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
+       [false,NUri.uri_of_string "cic:/matita/pts/Type0.univ"])
     | CicNotationPt.Sort (`NType s) -> NCic.Sort (NCic.Type
        [false,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
+    | CicNotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type
+       [false,NUri.uri_of_string ("cic:/matita/pts/CProp" ^ s ^ ".univ")])
     | CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string "cic:/matita/pts/CProp.univ"])
+       [false,NUri.uri_of_string "cic:/matita/pts/CProp0.univ"])
     | CicNotationPt.Symbol (symbol, instance) ->
         Disambiguate.resolve ~env ~mk_choice 
          (Symbol (symbol, instance)) (`Args [])
@@ -570,19 +574,20 @@ let interpretate_obj
      add_params
       (interpretate_term ~obj_context:[] ~context ~env ~uri:None
         ~is_path:false ty) in
+    let nref =
+     NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in
+    let obj_context = [name,nref] in
     let fields' =
      snd (
       List.fold_left
        (fun (context,res) (name,ty,_coercion,_arity) ->
          let ty =
-          interpretate_term ~obj_context:[] ~context ~env ~uri:None
+          interpretate_term ~obj_context ~context ~env ~uri:None
            ~is_path:false ty in
          let context' = (name,NCic.Decl ty)::context in
           context',(name,ty)::res
        ) (context,[]) fields) in
     let concl =
-     let nref =
-      NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in
      let mutind = NCic.Const nref in
      if params = [] then mutind
      else
@@ -646,6 +651,7 @@ let disambiguate_obj
    in
     List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
 ;;
+(*
 let _ = 
 let mk_type n = 
   if n = 0 then
@@ -684,4 +690,5 @@ in
          NCicEnvironment.add_constraint false (mk_type 3) (mk_cprop 3);
 
 ;;
+*)