Matitaweb:

[helm.git] / matitaB / components / grafite_engine / grafiteEngine.ml

diff --git a/matitaB/components/grafite_engine/grafiteEngine.ml b/matitaB/components/grafite_engine/grafiteEngine.ml
index bcbaa93ad39db76ec22bfe2411902f6dd8ddf7dc..02dfb00127adddb88455891d20ff78e87f82715e 100644 (file)
--- 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')) 
 ;;