Merge PR #6328: Fix #6313: lost goals in nested ltac in refine

2 files changed, 6 insertions, 0 deletions

diff --git a/clib/option.ml b/clib/option.ml
index 21913e8f7a..32fe2fc5f5 100644
--- a/clib/option.ml
+++ b/clib/option.ml
@@ -52,6 +52,9 @@ let get = function
 (** [make x] returns [Some x]. *)
 let make x = Some x
 
+(** [bind x f] is [f y] if [x] is [Some y] and [None] otherwise *)
+let bind x f = match x with Some y -> f y | None -> None
+
 (** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *)
 let init b x =
   if b then
diff --git a/clib/option.mli b/clib/option.mli
index 2260993526..67b42268a7 100644
--- a/clib/option.mli
+++ b/clib/option.mli
@@ -43,6 +43,9 @@ val get : 'a option -> 'a
 (** [make x] returns [Some x]. *)
 val make : 'a -> 'a option
 
+(** [bind x f] is [f y] if [x] is [Some y] and [None] otherwise *)
+val bind : 'a option -> ('a -> 'b option) -> 'b option
+
 (** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *)
 val init : bool -> 'a -> 'a option