diff options
Diffstat (limited to 'hol-light/pg_tactics.ml')
| -rw-r--r-- | hol-light/pg_tactics.ml | 8 |
1 files changed, 6 insertions, 2 deletions
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 ())));; |