X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=f320db2cc3942b18fbbd356cc924f6d204af867a;hb=4c2a5e7da43e15d9a5f35d65f6bd6eda9a117d93;hp=f1d53de52f217171b267800774ceea9959f0293d;hpb=cf3635c0830661f59d16339cd7fc9c3b948fcbc8;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index f1d53de52..f320db2cc 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 open Printf
 
 open DisambiguateTypes
@@ -409,7 +411,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
     | None -> Cic.Implicit annotation
     | Some term -> aux ~localize loc context term
   in
-   aux ~localize:true dummy_floc context ast
+   aux ~localize:true HExtlib.dummy_floc context ast
 
 let interpretate_path ~context path =
  let localization_tbl = Cic.CicHash.create 23 in
@@ -445,15 +447,6 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
           i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
         ) (0,[]) tyl) in
      let con_env = DisambiguateTypes.env_of_list name_to_uris env in
-     let undebrujin t =
-      snd
-       (List.fold_right
-         (fun (name,_,_,_) (i,t) ->
-           (*here the explicit_named_substituion is assumed to be of length 0 *)
-           let t' = Cic.MutInd (uri,i,[])  in
-           let t = CicSubstitution.subst t' t in
-            i - 1,t
-         ) tyl (List.length tyl - 1,t)) in
      let tyl =
       List.map
        (fun (name,b,ty,cl) ->
@@ -464,7 +457,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
              let ty' =
               add_params (interpretate_term context con_env None false ty)
              in
-              name,undebrujin ty'
+              name,ty'
            ) cl
          in
           name,b,ty',cl'
@@ -545,7 +538,7 @@ let rev_uniq =
 (* "aux" keeps domain in reverse order and doesn't care about duplicates.
  * Domain item more in deep in the list will be processed first.
  *)
-let rec domain_rev_of_term ?(loc = dummy_floc) context = function
+let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function
   | CicNotationPt.AttributedTerm (`Loc loc, term) ->
      domain_rev_of_term ~loc context term
   | CicNotationPt.AttributedTerm (_, term) ->