X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;fp=matitaB%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=02dfb00127adddb88455891d20ff78e87f82715e;hb=c81b0e8dbfe80e2350e9322afa8316f39f98c3b3;hp=bcbaa93ad39db76ec22bfe2411902f6dd8ddf7dc;hpb=935c8d1b73726bb49b99e5c2dbebdea0d617fa1a;p=helm.git

diff --git a/matitaB/components/grafite_engine/grafiteEngine.ml b/matitaB/components/grafite_engine/grafiteEngine.ml
index bcbaa93ad..02dfb0012 100644
--- a/matitaB/components/grafite_engine/grafiteEngine.ml
+++ b/matitaB/components/grafite_engine/grafiteEngine.ml
@@ -34,7 +34,7 @@ type options = {
   do_heavy_checks: bool ; 
 }
 
-let prerr_endline _ = ()
+let prerr_endline _ = () 
 
 let basic_eval_unification_hint (t,n) status =
  NCicUnifHint.add_user_provided_hint status t n
@@ -136,12 +136,13 @@ let eval_alias status data=
 let basic_eval_input_notation (l1,l2) status =
   GrafiteParser.extend status l1 
    (fun env loc ->
-     let rec get_disamb = function
+     (* let rec get_disamb = function
      | [] -> Stdpp.dummy_loc,None,None
-     | (_,(NotationEnv.NoType,NotationEnv.DisambiguationValue dv))::_ -> dv
+     | (_,(csym,NotationEnv.NoType,NotationEnv.DisambiguationValue dv))::_ -> dv
      | _::tl -> get_disamb tl
-     in
-     let l2' = TermContentPres.instantiate_level2 status env (get_disamb env) l2 in
+     in *)
+     let l2' = 
+       TermContentPres.instantiate_level2 status env (*(get_disamb env)*) l2 in
      prerr_endline ("new l2 ast : " ^ (NotationPp.pp_term status l2'));
      NotationPt.AttributedTerm (`Loc loc,l2')) 
 ;;