From ef2ce75bdb5c78aad5ae4b2a1ff94e539fc10e0c Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 8 Feb 2012 15:57:56 +0000 Subject: Try to make evars output match what is expected by Prooftree --- hol-light/pg_tactics.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'hol-light') diff --git a/hol-light/pg_tactics.ml b/hol-light/pg_tactics.ml index d0e4f2ce..c54626b7 100644 --- a/hol-light/pg_tactics.ml +++ b/hol-light/pg_tactics.ml @@ -131,11 +131,15 @@ let (print_xgoalstack:goalstack->unit) = (vs,theta) in let foo v = let (x,_) = dest_var v in - x ^ if (can (rev_assoc v) theta) then " using" else " open" in + "?" (* FIXME: Coq syntax for meta vars is expected by Prooftree *) + ^ x ^ if (can (rev_assoc v) theta) then " using" else " open" in let xs = map foo vs in (print_newline(); print_string "(dependent evars:"; - print_string_seplist ", " xs; + if xs != [] then + (print_string " "; + print_string_seplist ", " xs; + print_string ","); print_string ")"; print_newline ())));; -- cgit v1.2.3