X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=63f1eee58483af12e3dc946e2dd1d83da36ec930;hb=HEAD;hp=24e69a43d9e37d4699182bc5de4df30e88e8c40c;hpb=53b8e2af661ad4165aa0b1deccd0a7522d96ce2e;p=helm.git

diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml
index 24e69a43d..63f1eee58 100644
--- a/matita/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml
@@ -103,7 +103,7 @@ let find_in_context name context =
   aux 1 context
 
 let interpretate_term_and_interpretate_term_option (status: #NCic.status)
-  ?(create_dummy_ids=false) ~obj_context ~mk_choice ~env ~uri ~is_path
+  ~create_dummy_ids ~obj_context ~mk_choice ~env ~uri ~is_path
   ~localization_tbl 
 =
   (* create_dummy_ids shouldbe used only for interpretating patterns *)
@@ -167,7 +167,8 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
                    "branch pattern must be \"_\"")))
            ) branches in
          let indtype_ref =
-          NReference.reference_of_string "cic:/fake_indty.ind(0,0,0)"
+          let uri = NUri.uri_of_string "cic:/matita/dummy/indty.ind" in 
+          NRef.reference_of_spec uri (NRef.Ind (true,1,1))
          in
           NCic.Match (indtype_ref, cic_outtype, cic_term,
            (List.map do_branch branches))
@@ -177,7 +178,7 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
           | Some (indty_ident, _) ->
              (match Disambiguate.resolve ~env ~mk_choice 
                 (DT.Id indty_ident) (`Args []) with
-              | NCic.Const (NReference.Ref (_,NReference.Ind _) as r) -> r
+              | NCic.Const (NRef.Ref (_,NRef.Ind _) as r) -> r
               | NCic.Implicit _ ->
                  raise (Disambiguate.Try_again 
                   (lazy "The type of the term to be matched is still unknown"))
@@ -205,9 +206,9 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
 *)
               (match Disambiguate.resolve ~env ~mk_choice
                 (DT.Id (fst_constructor branches)) (`Args []) with
-              | NCic.Const (NReference.Ref (_,NReference.Con _) as r) -> 
+              | NCic.Const (NRef.Ref (_,NRef.Con _) as r) -> 
                    let b,_,_,_,_= NCicEnvironment.get_checked_indtys status r in
-                   NReference.mk_indty b r
+                   NRef.mk_indty b r
               | NCic.Implicit _ ->
                  raise (Disambiguate.Try_again 
                   (lazy "The type of the term to be matched is still unknown"))
@@ -322,7 +323,7 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
     | NotationPt.Uri (uri, subst) ->
        assert (subst = None);
        (try
-         NCic.Const (NReference.reference_of_string uri)
+         NCic.Const (NRef.reference_of_string uri)
         with NRef.IllFormedReference _ ->
          NotationPt.fail loc "Ill formed reference")
     | NotationPt.NRef nref -> NCic.Const nref
@@ -439,7 +440,7 @@ let interpretate_obj status
              ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
           in
           NCic.Constant ([],name,Some bo,ty',attrs))
- | NotationPt.Inductive (params,tyl) ->
+ | NotationPt.Inductive (params,tyl,source) ->
     let context,params =
      let context,res =
       List.fold_left
@@ -466,7 +467,7 @@ let interpretate_obj status
       List.fold_left
        (fun (i,res) (name,_,_,_) ->
          let nref =
-          NReference.reference_of_spec uri (NReference.Ind (inductive,i,leftno))
+          NRef.reference_of_spec uri (NRef.Ind (inductive,i,leftno))
          in
           i+1,(name,nref)::res)
        (0,[]) tyl) in
@@ -492,10 +493,10 @@ let interpretate_obj status
       ) tyl
     in
      let height = (* XXX calculate *) 0 in
-     let attrs = `Provided, `Regular in
+     let attrs = source, `Regular in
      uri, height, [], [], 
      NCic.Inductive (inductive,leftno,tyl,attrs)
- | NotationPt.Record (params,name,ty,fields) ->
+ | NotationPt.Record (params,name,ty,fields,source) ->
     let context,params =
      let context,res =
       List.fold_left
@@ -521,7 +522,7 @@ let interpretate_obj status
       (interpretate_term status ~obj_context:[] ~context ~env ~uri:None
         ~is_path:false ty) in
     let nref =
-     NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in
+     NRef.reference_of_spec uri (NRef.Ind (true,0,leftno)) in
     let obj_context = [name,nref] in
     let fields' =
      snd (
@@ -546,7 +547,7 @@ let interpretate_obj status
     let tyl = [relevance,name,ty',[relevance,"mk_" ^ name,con']] in
     let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
      let height = (* XXX calculate *) 0 in
-     let attrs = `Provided, `Record field_names in
+     let attrs = source, `Record field_names in
      uri, height, [], [], 
      NCic.Inductive (true,leftno,tyl,attrs)
  | NotationPt.LetRec (kind, defs, attrs) ->
@@ -555,9 +556,9 @@ let interpretate_obj status
        List.fold_left
          (fun (i,acc) (_,(name,_),_,k) -> 
           (i+1, 
-            (ncic_name_of_ident name, NReference.reference_of_spec uri 
-             (if inductive then NReference.Fix (i,k,0)
-              else NReference.CoFix i)) :: acc))
+            (ncic_name_of_ident name, NRef.reference_of_spec uri 
+             (if inductive then NRef.Fix (i,k,0)
+              else NRef.CoFix i)) :: acc))
          (0,[]) defs
      in
      let inductiveFuns =
@@ -601,7 +602,7 @@ let disambiguate_term (status: #NCicCoercion.status) ~context ~metasenv ~subst
      ~universe ~uri:None ~pp_thing:(NotationPp.pp_term status)
      ~passes:(MultiPassDisambiguator.passes ())
      ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
-     ~interpretate_thing:(interpretate_term status ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
+     ~interpretate_thing:(interpretate_term status ~obj_context:[] ~mk_choice ?create_dummy_ids:None)
      ~refine_thing:(refine_term status) (text,prefix_len,term)
      ~mk_localization_tbl ~expty ~subst
    in