Simplified rendering

[helm.git] / matitaB / components / content / notationPp.ml

diff --git a/matitaB/components/content/notationPp.ml b/matitaB/components/content/notationPp.ml
index 8f1db4a62e3ef2311fcba6f41b0b3d6751a75f18..082a5ddf81d16d40ca9249b93300b72eb8f54df7 100644 (file)
--- a/matitaB/components/content/notationPp.ml
+++ b/matitaB/components/content/notationPp.ml
@@ -184,10 +184,6 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
     | true, Ast.Ident _    -> t_pp
     | _                    -> sprintf "(%s)" t_pp
 
-and pp_subst status (name, term) =
- sprintf "%s \\Assign %s" name (pp_term status term)
-and pp_substs status substs = String.concat "; " (List.map (pp_subst status) substs)
-
 and pp_pattern status =
  function
     Ast.Pattern (head, href, vars), term ->