added \to notation for anonymous binders Pi and Lambda

[helm.git] / helm / ocaml / cic_transformations / cicAstPp.ml

diff --git a/helm/ocaml/cic_transformations/cicAstPp.ml b/helm/ocaml/cic_transformations/cicAstPp.ml
index b1e6588766beeeb2b9b3fa1414cdfb2e06ec5871..ee60c427963aa3a191cd4f06c25451330b2b3c8b 100644 (file)
--- a/helm/ocaml/cic_transformations/cicAstPp.ml
+++ b/helm/ocaml/cic_transformations/cicAstPp.ml
@@ -38,6 +38,11 @@ let rec pp_term = function
 
   | CicAst.Appl terms ->
       sprintf "(%s)" (String.concat " " (List.map pp_term terms))
+  | CicAst.Binder (`Forall, (Cic.Anonymous, typ), body)
+  | CicAst.Binder (`Pi, (Cic.Anonymous, typ), body) ->
+      sprintf "(%s \\to %s)"
+        (match typ with None -> "?" | Some typ -> pp_term typ)
+        (pp_term body)
   | CicAst.Binder (kind, var, body) ->
       sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var)
         (pp_term body)