X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_disambiguation%2Fdisambiguate.ml;h=e93c54808298f14879396fbf637c3444c5bd775f;hb=5717dca7637e00f6f82e462619ee0e07d99cf289;hp=5c198cb5962bf06bef7850892ba384ffe2c35618;hpb=e134b6f156268364d3027e73910c19e9c7e09838;p=helm.git

diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml
index 5c198cb59..e93c54808 100644
--- a/components/cic_disambiguation/disambiguate.ml
+++ b/components/cic_disambiguation/disambiguate.ml
@@ -86,7 +86,7 @@ let uniq_domain dom =
  in
   snd (aux [] dom)
 
-let debug = true
+let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 (*
@@ -172,9 +172,10 @@ let find_in_context name context =
   in
   aux 1 context
 
-let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
+let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~uri ~is_path ast
      ~localization_tbl
 =
+  (* create_dummy_ids shouldbe used only for interpretating patterns *)
   assert (uri = None);
   let rec aux ~localize loc (context: Cic.name list) = function
     | CicNotationPt.AttributedTerm (`Loc loc, term) ->
@@ -217,6 +218,9 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
           do_branch' context args
         in
         let (indtype_uri, indtype_no) =
+          if create_dummy_ids then
+            (UriManager.uri_of_string "cic:/fake_indty.con", 0)
+          else
           match indty_ident with
           | Some (indty_ident, _) ->
              (match resolve env (Id indty_ident) () with
@@ -459,7 +463,8 @@ let interpretate_path ~context path =
  let localization_tbl = Cic.CicHash.create 23 in
   (* here we are throwing away useful localization informations!!! *)
   fst (
-   interpretate_term ~context ~env:Environment.empty ~uri:None ~is_path:true
+   interpretate_term ~create_dummy_ids:true 
+    ~context ~env:Environment.empty ~uri:None ~is_path:true
     path ~localization_tbl, localization_tbl)
 
 let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
@@ -684,7 +689,7 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
                   CicNotationUtil.cic_name_of_name var :: context,
                   domain_of_term_option ~loc ~context ty @ res)
                 (add_defs context,[]) params))
-            @ domain_of_term_option ~loc ~context typ
+            @ domain_of_term_option ~loc ~context:context' typ
             @ domain_of_term ~loc ~context:context' body
           ) [] defs
       in
@@ -809,7 +814,7 @@ module type Disambiguator =
 sig
   val disambiguate_term :
     ?fresh_instances:bool ->
-    dbd:HMysql.dbd ->
+    dbd:HSql.dbd ->
     context:Cic.context ->
     metasenv:Cic.metasenv ->
     ?initial_ugraph:CicUniv.universe_graph -> 
@@ -824,7 +829,7 @@ sig
 
   val disambiguate_obj :
     ?fresh_instances:bool ->
-    dbd:HMysql.dbd ->
+    dbd:HSql.dbd ->
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     uri:UriManager.uri option ->     (* required only for inductive types *)
@@ -1184,7 +1189,7 @@ in refine_profiler.HExtlib.profile foo ()
       disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
         ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
         ~domain_of_thing:domain_of_term
-        ~interpretate_thing:interpretate_term
+        ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
         ~refine_thing:refine_term (text,prefix_len,term)
 
     let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri