Changes to disambiguation:

[helm.git] / matitaB / components / grafite / grafiteAstPp.ml

diff --git a/matitaB/components/grafite/grafiteAstPp.ml b/matitaB/components/grafite/grafiteAstPp.ml
index c4993712754443227cec682337fbbc64567be17f..d4d312bd2b455c38489f81c50ee53e046f1cfd0f 100644 (file)
--- a/matitaB/components/grafite/grafiteAstPp.ml
+++ b/matitaB/components/grafite/grafiteAstPp.ml
@@ -59,7 +59,7 @@ let rec pp_ntactic status ~map_unicode_to_tex =
   | NAuto (_,(None,flgs)) ->
       "nautobatch" ^
         String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
-  | NAuto (_,(Some l,flgs)) ->
+  | NAuto (_,(Some (_,l),flgs)) ->
       "nautobatch" ^ " by " ^
          (String.concat "," (List.map (NotationPp.pp_term status) l)) ^
         String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
@@ -167,7 +167,7 @@ let pp_ncommand status = function
   | NUnivConstraint (_) -> "not supported"
   | NCoercion (_) -> "not supported"
   | NObj (_,obj) -> NotationPp.pp_obj (NotationPp.pp_term status) obj
-  | NQed (_) -> "nqed"
+  | NQed (_,_) -> "nqed"
   | NCopy (_,name,uri,map) -> 
       "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^ 
         String.concat " and "