Commit bae98fea authored by Raphael Cauderlier's avatar Raphael Cauderlier

Add goal and context information on no-such-assumption exceptions

This is intended to help debugging failure of the "assumption"
certificate combinator and similar ones built on top of with_variable
and with_assumption.  The user can herself see why the goal is not one
of the assumptions.
parent b36fb641
......@@ -50,10 +50,13 @@ instead of the goal. ;)
with_context : (context -> certificate) -> certificate.
[A,G,c] run A G (with_context c) --> run A G (c G).
no_successful_assumption : tac.exc.
no_successful_assumption : fol.prop -> context -> tac.exc.
def try_all_assumptions : (A : prop -> proof A -> certificate) ->
context -> certificate.
[] try_all_assumptions _ nil_ctx --> raise no_successful_assumption
[] try_all_assumptions _ nil_ctx -->
with_goal (A =>
with_context (G =>
raise (no_successful_assumption A G)))
[f,G]
try_all_assumptions f (cons_ctx_var _ _ G)
-->
......@@ -79,9 +82,12 @@ def ctx_remove : prop -> context -> context.
clear : prop -> certificate -> certificate.
[A,G,B,c] run A G (clear B c) --> run A (ctx_remove B G) c.
no_successful_variable : tac.exc.
no_successful_variable : fol.prop -> context -> tac.exc.
def try_all_variables : (A : type -> term A -> certificate) -> context -> certificate.
[] try_all_variables _ nil_ctx --> raise no_successful_variable
[] try_all_variables _ nil_ctx -->
with_goal (A =>
with_context (G =>
raise (no_successful_variable A G)))
[f,A,a,G]
try_all_variables f (cons_ctx_var A a G)
-->
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment