]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/cicAstPp.ml
differentieted empty substitution list from no substitution given
[helm.git] / helm / ocaml / cic_transformations / cicAstPp.ml
index 02cf5511cd963a07b84c4c65b3902b0fde0f62fb..bd9eea6012927c97c6a64f0cb8fdf8d8483a6117 100644 (file)
@@ -62,8 +62,10 @@ let rec pp_term = function
               sprintf "%s = %s" (pp_capture_variable var) (pp_term body))
             definitions))
         (pp_term term)
-  | CicAst.Ident (name, []) -> name
-  | CicAst.Ident (name, substs) -> sprintf "%s[%s]" name (pp_substs substs)
+  | CicAst.Ident (name, Some [])
+  | CicAst.Ident (name, None) ->
+      name
+  | CicAst.Ident (name, Some substs) -> sprintf "%s[%s]" name (pp_substs substs)
   | CicAst.Implicit -> "?"
   | CicAst.Meta (index, substs) ->
       sprintf "%d[%s]" index