Syntax of explicit named substitions syncronized with the parser.

diff --git a/helm/ocaml/cic_transformations/cicAstPp.ml b/helm/ocaml/cic_transformations/cicAstPp.ml
index bd9eea6012927c97c6a64f0cb8fdf8d8483a6117..a854234b78eb1b6be7e40568ec59d86294183ed3 100644 (file)
--- a/helm/ocaml/cic_transformations/cicAstPp.ml
+++ b/helm/ocaml/cic_transformations/cicAstPp.ml
@@ -65,7 +65,7 @@ let rec pp_term = function
   | CicAst.Ident (name, Some [])
   | CicAst.Ident (name, None) ->
       name
-  | CicAst.Ident (name, Some substs) -> sprintf "%s[%s]" name (pp_substs substs)
+  | CicAst.Ident (name, Some substs) -> sprintf "%s \\subst [%s]" name (pp_substs substs)
   | CicAst.Implicit -> "?"
   | CicAst.Meta (index, substs) ->
       sprintf "%d[%s]" index
@@ -78,7 +78,7 @@ let rec pp_term = function
   | CicAst.Sort `CProp -> "CProp"
   | CicAst.Symbol (name, _) -> name
 
-and pp_subst (name, term) = sprintf "%s := %s" name (pp_term term)
+and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term)
 and pp_substs substs = String.concat "; " (List.map pp_subst substs)
 
 and pp_pattern ((head, vars), term) =