diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2012-02-08 15:57:56 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2012-02-08 15:57:56 +0000 |
| commit | ef2ce75bdb5c78aad5ae4b2a1ff94e539fc10e0c (patch) | |
| tree | 8acc878ece5f7ea691c19368baabdea72fe85b4b /hol-light | |
| parent | 7cc95a00fda26cbd6694075dca74b16c6c54f016 (diff) | |
Try to make evars output match what is expected by Prooftree
Diffstat (limited to 'hol-light')
| -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 ())));; |