From e61bf3a95901c62c7b891fb58b176ac38fb7d8e4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 5 Mar 2004 12:24:05 +0000 Subject: [PATCH 1/1] Syntax of explicit named substitions syncronized with the parser. --- helm/ocaml/cic_transformations/cicAstPp.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic_transformations/cicAstPp.ml b/helm/ocaml/cic_transformations/cicAstPp.ml index bd9eea601..a854234b7 100644 --- 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) = -- 2.39.2