X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;fp=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=e69099cb5d30dda0527de4f4403c4e8727de3255;hb=9a0e4f3be9f70662f18d2d3b6dd60ae79fba565b;hp=3acfd39043e26cab9d7c2ff8f6275cce73f3fd83;hpb=f59550b5a9cdddbb348697201fae7d736d6b96c5;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 3acfd3904..e69099cb5 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -364,7 +364,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj =
  assert (context = []);
  assert (is_path = false);
  match obj with
-  | GrafiteAst.Inductive (params,tyl) ->
+  | CicNotationPt.Inductive (params,tyl) ->
      let uri = match uri with Some uri -> uri | None -> assert false in
      let context,params =
       let context,res =
@@ -412,7 +412,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj =
        ) tyl
      in
       Cic.InductiveDefinition (tyl,[],List.length params,[])
-  | GrafiteAst.Record (params,name,ty,fields) ->
+  | CicNotationPt.Record (params,name,ty,fields) ->
      let uri = match uri with Some uri -> uri | None -> assert false in
      let context,params =
       let context,res =
@@ -450,7 +450,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj =
      let field_names = List.map fst fields in
       Cic.InductiveDefinition
        (tyl,[],List.length params,[`Class (`Record field_names)])
-  | GrafiteAst.Theorem (flavour, name, ty, bo) ->
+  | CicNotationPt.Theorem (flavour, name, ty, bo) ->
      let attrs = [`Flavour flavour] in
      let ty' = interpretate_term [] env None false ty in
      (match bo with
@@ -601,12 +601,12 @@ let domain_of_obj ~context ast =
  assert (context = []);
  let domain_rev =
   match ast with
-   | GrafiteAst.Theorem (_,_,ty,bo) ->
+   | CicNotationPt.Theorem (_,_,ty,bo) ->
       (match bo with
           None -> []
         | Some bo -> domain_rev_of_term [] bo) @
       domain_of_term [] ty
-   | GrafiteAst.Inductive (params,tyl) ->
+   | CicNotationPt.Inductive (params,tyl) ->
       let dom =
        List.flatten (
         List.rev_map
@@ -626,7 +626,7 @@ let domain_of_obj ~context ast =
           not (  List.exists (fun (name',_) -> name = Id name') params
               || List.exists (fun (name',_,_,_) -> name = Id name') tyl)
         ) dom
-   | GrafiteAst.Record (params,_,ty,fields) ->
+   | CicNotationPt.Record (params,_,ty,fields) ->
       let dom =
        List.flatten
         (List.rev_map (fun (_,ty) -> domain_rev_of_term [] ty) fields) in
@@ -676,7 +676,7 @@ sig
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     uri:UriManager.uri option ->     (* required only for inductive types *)
-    GrafiteAst.obj ->
+    CicNotationPt.obj ->
     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.obj *
@@ -752,7 +752,7 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
               | Id id -> choices_of_id dbd id
               | Symbol (symb, _) ->
                   List.map DisambiguateChoices.mk_choice
-                    (CicNotationRew.lookup_interpretations symb)
+                    (TermAcicContent.lookup_interpretations symb)
               | Num instance ->
                   DisambiguateChoices.lookup_num_choices ()
             in
@@ -942,7 +942,7 @@ in refine_profiler.HExtlib.profile foo ()
         if fresh_instances then CicNotationUtil.freshen_obj obj else obj
       in
       disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
-        ~pp_thing:GrafiteAstPp.pp_obj ~domain_of_thing:domain_of_obj
+        ~pp_thing:CicNotationPp.pp_obj ~domain_of_thing:domain_of_obj
         ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
         obj
   end