Commit a4095ae5 authored by Raphael Cauderlier's avatar Raphael Cauderlier

Abbreviation for tac.run followed by cert.run.

parent bd560f72
......@@ -378,6 +378,7 @@ a tactic attempting to prove the goal formula.
- =cert.cons_ctx_proof : A : fol.prop -> fol.proof A -> cert.context -> cert.context=
- =cert.certificate : Type=
- =cert.run : A : fol.prop -> cert.context -> cert.certificate -> tac.tactic A=
- =cert.cert_run : A : fol.prop -> cert.certificate -> fol.proof A=
** Certificate primitives
......
......@@ -23,6 +23,8 @@ cons_ctx_proof : A : prop -> proof A -> context -> context.
certificate : Type.
def run : A : prop -> context -> certificate -> tac.tactic A.
def cert_run (A : prop) (c : certificate) : fol.proof A :=
tac.run A (cert.run A nil_ctx c).
(; exact A a proves G |- A for any G ;)
exact_mismatch : prop -> prop -> tac.exc.
......
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