Adding variants enter_one and refine_one which assume that exactly one

goal is under focus and which support returning a relevant output.

4 files changed, 42 insertions, 6 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 576569cf5..a2838a2de 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1058,6 +1058,26 @@ module Goal = struct
     end
     end
 
+  exception NotExactlyOneSubgoal
+  let _ = CErrors.register_handler begin function
+  | NotExactlyOneSubgoal ->
+      CErrors.errorlabstrm "" (Pp.str"Not exactly one subgoal.")
+  | _ -> raise CErrors.Unhandled
+  end
+
+  let enter_one f =
+    let open Proof in
+    Comb.get >>= function
+    | [goal] -> begin
+       Env.get >>= fun env ->
+       tclEVARMAP >>= fun sigma ->
+       try f.enter (gmake env sigma goal)
+       with e when catchable_exception e ->
+         let (e, info) = CErrors.push e in
+         tclZERO ~info e
+      end
+    | _ -> tclZERO NotExactlyOneSubgoal
+
   type ('a, 'b) s_enter =
     { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma }
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 901cf26e0..bc68f11ff 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -499,6 +499,10 @@ module Goal : sig
   (** Like {!nf_enter}, but does not normalize the goal beforehand. *)
   val enter : ([ `LZ ], unit tactic) enter -> unit tactic
 
+  (** Like {!enter}, but assumes exactly one goal under focus, raising *)
+  (** an error otherwise. *)
+  val enter_one : ([ `LZ ], 'a tactic) enter -> 'a tactic
+
   type ('a, 'b) s_enter =
     { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma }
 
diff --git a/proofs/refine.ml b/proofs/refine.ml
index af9be7897..dc6f4cea1 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -51,7 +51,8 @@ let typecheck_proof c concl env sigma =
 let (pr_constrv,pr_constr) =
   Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
 
-let refine ?(unsafe = true) f = Proofview.Goal.enter { enter = begin fun gl ->
+let make_refine_enter ?(unsafe = true) f =
+  { enter = fun gl ->
   let gl = Proofview.Goal.assume gl in
   let sigma = Proofview.Goal.sigma gl in
   let sigma = Sigma.to_evar_map sigma in
@@ -62,7 +63,7 @@ let refine ?(unsafe = true) f = Proofview.Goal.enter { enter = begin fun gl ->
   let prev_future_goals = Evd.future_goals sigma in
   let prev_principal_goal = Evd.principal_future_goal sigma in
   (** Create the refinement term *)
-  let (c, sigma) = Sigma.run (Evd.reset_future_goals sigma) f in
+  let ((v,c), sigma) = Sigma.run (Evd.reset_future_goals sigma) f in
   let evs = Evd.future_goals sigma in
   let evkmain = Evd.principal_future_goal sigma in
   (** Check that the introduced evars are well-typed *)
@@ -92,10 +93,18 @@ let refine ?(unsafe = true) f = Proofview.Goal.enter { enter = begin fun gl ->
   let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in
   let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in
   let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in
-  Proofview.Trace.name_tactic trace (Proofview.tclUNIT ()) >>= fun () ->
-  Proofview.Unsafe.tclEVARS sigma >>= fun () ->
-  Proofview.Unsafe.tclSETGOALS comb
-end }
+  Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v ->
+  Proofview.Unsafe.tclEVARS sigma <*>
+  Proofview.Unsafe.tclSETGOALS comb <*>
+  Proofview.tclUNIT v
+  }
+
+let refine_one ?(unsafe = true) f =
+  Proofview.Goal.enter_one (make_refine_enter ~unsafe f)
+
+let refine ?(unsafe = true) f =
+  let f = { run = fun sigma -> let Sigma (c,sigma,p) = f.run sigma in Sigma (((),c),sigma,p) } in
+  Proofview.Goal.enter (make_refine_enter ~unsafe f)
 
 (** Useful definitions *)
 
diff --git a/proofs/refine.mli b/proofs/refine.mli
index a9798b704..3d140f036 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -30,6 +30,9 @@ val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
     tactic failures. If [unsafe] is [false] (default is [true]) [t] is
     type-checked beforehand. *)
 
+val refine_one : ?unsafe:bool -> ('a * Constr.t) Sigma.run -> 'a tactic
+(** A generalization of [refine] which assumes exactly one goal under focus *)
+
 (** {7 Helper functions} *)
 
 val with_type : Environ.env -> Evd.evar_map ->