]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/applyTransformation.ml
Most warnings turned into errors and avoided
[helm.git] / matita / matita / applyTransformation.ml
index 705ef7936df0b993176d11093c6f03b7104004c7..50d7d25bf8f7ab5c26166e6d0a22f23db0d7b25c 100644 (file)
@@ -66,7 +66,7 @@ let ntxt_of_cic_context ~metasenv ~subst =
   Content2pres.ncontext2pres
   ((new NCicPp.status)#ppcontext ~metasenv ~subst)
 
-let ntxt_of_cic_subst ~map_unicode_to_tex size status ~metasenv ?use_subst subst =
+let ntxt_of_cic_subst ~map_unicode_to_tex:_ _size _status ~metasenv ?use_subst subst =
  [],
  "<<<high level printer for subst not implemented; low-level printing:>>>\n" ^
   (new NCicPp.status)#ppsubst ~metasenv ?use_subst subst
@@ -75,24 +75,24 @@ class status =
  object(self)
   inherit Interpretations.status
   inherit TermContentPres.status
-  method ppterm ~context ~subst ~metasenv ?margin ?inside_fix t =
-   snd (ntxt_of_cic_term ~map_unicode_to_tex:true 80 self ~metasenv ~subst
+  method ppterm ~context ~subst ~metasenv ?margin:(_) ?inside_fix:(_) t =
+   snd (ntxt_of_cic_term ~map_unicode_to_tex:false 80 self ~metasenv ~subst
     ~context t)
 
-  method ppcontext ?sep ~subst ~metasenv context =
-   snd (ntxt_of_cic_context ~map_unicode_to_tex:true 80 self ~metasenv ~subst
+  method ppcontext ?sep:(_) ~subst ~metasenv context =
+   snd (ntxt_of_cic_context ~map_unicode_to_tex:false 80 self ~metasenv ~subst
     context)
 
   method ppsubst ~metasenv ?use_subst subst =
-   snd (ntxt_of_cic_subst ~map_unicode_to_tex:true 80 self ~metasenv ?use_subst
+   snd (ntxt_of_cic_subst ~map_unicode_to_tex:false 80 self ~metasenv ?use_subst
     subst)
 
   method ppmetasenv ~subst metasenv =
    String.concat "\n"
     (List.map
-      (fun m -> snd (ntxt_of_cic_sequent ~map_unicode_to_tex:true 80 self
+      (fun m -> snd (ntxt_of_cic_sequent ~map_unicode_to_tex:false 80 self
         ~metasenv ~subst m)) metasenv)
 
   method ppobj obj =
-   snd (ntxt_of_cic_object ~map_unicode_to_tex:true 80 self obj)
+   snd (ntxt_of_cic_object ~map_unicode_to_tex:false 80 self obj)
  end