Small modifications of evalwrapLib from the P4 project

[didriklundberg]

The suggested changes are as follows:

• No GEN_ALL done at the end of eval_ctxt_gen. Rationale: for the step-wise evaluation-under-assumptions, I take the result of eval_ctxt_gen and use it with MATCH_MP, for which I don't want any enclosing universal quantifier, but free variables. If you want GEN_ALL of the result it's trivial to add it anyhow, but it just adds inefficiency if it's the default if you always need to reverse it. Maybe another wrapper can be added that also does GEN_ALL if this is the preferred format for another project?
• ctxt parameter of eval_ctxt_gen changed to type thm from type term list. Rationale: Similarly to the previous point, if eval_ctxt_gen is used inside a loop with the same ctxt every time, it's inefficient to do map ASSUME and LIST_CONJ every time.
  • The interface of qeval_ctxt is unchanged by making compensations to the call of eval_ctxt_gen - other new wrappers like this can be created if needed.
  • dest_conj_list is no longer needed due to this change
  • Swapped the DISCH_ALL at the end for a DISCH_CONJUNCTS_ALL to match the new format

IMO in general when you program some core functionality that's called by means of different wrappers, it's a good idea to build in the least amount of format conversions into it. Then you can split the ways of calling the mechanism into those most suitable for computation and convenience and add in the extra stuff in the latter.

[arolle]

Thanks for the improvements. It would be really nice if you generally could add a simple example that demonstrates your usage.