Skip to content

Commit 22a9cf8

Browse files
Added documentation comment
1 parent f930f16 commit 22a9cf8

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

TypeTheory/Auxiliary/Partial.v

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -352,6 +352,7 @@ Section Monad.
352352

353353
End Monad.
354354

355+
(* TODO: make these more consistent in naming with similar monadic tactic family [unsquash]? *)
355356
Ltac get_partial t x := apply (bind_partial t); intros x.
356357
(** [get_partial t x]: like Haskell’s [x <- t]. *)
357358
Ltac destruct_partial x := apply (bind_partial x); clear x; intros x.

0 commit comments

Comments
 (0)