Commit 442326ee authored by charguer's avatar charguer

doc xclose

parent 0e0fd751
......@@ -966,6 +966,9 @@ Tactic Notation "xopenxs" constr(t) :=
- [xclose2 p] to perform [xclose p] twice.
- [xclose (>> p X Y)] where the extra arguments are used to
provide explicit arguments to instantiate the "closing" lemma.
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