Imported Upstream version 8.9.0upstream/8.9.0upstream

1 files changed, 13 insertions, 18 deletions

diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md
index 8f96ac22..77455223 100644
--- a/dev/doc/proof-engine.md
+++ b/dev/doc/proof-engine.md
@@ -42,8 +42,8 @@ goal holes thanks to the `Refine` module, and in particular to the
 `Refine.refine` primitive.
 
 ```ocaml
-val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic
-(** In [refine typecheck t], [t] is a term with holes under some
+val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
+(** In [refine ~typecheck t], [t] is a term with holes under some
     [evar_map] context. The term [t] is used as a partial solution
     for the current goal (refine is a goal-dependent tactic), the
     new holes created by [t] become the new subgoals. Exceptions
@@ -51,12 +51,11 @@ val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic
     tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *)
 ```
 
-In a first approximation, we can think of `'a Sigma.run` as
-`evar_map -> 'a * evar_map`. What the function does is first evaluate the
-`Constr.t Sigma.run` argument in the current proof state, and then use the
-resulting term as a filler for the proof under focus. All evars that have been
-created by the invocation of this thunk are then turned into new goals added in
-the order of their creation.
+What the function does is first evaluate the `t` argument in the
+current proof state, and then use the resulting term as a filler for
+the proof under focus. All evars that have been created by the
+invocation of this thunk are then turned into new goals added in the
+order of their creation.
 
 To see how we can use it, let us have a look at an idealized example, the `cut`
 tactic. Assuming `X` is a type, `cut X` fills the current goal `[Γ ⊢ _ : A]`
@@ -66,8 +65,7 @@ two new holes `[e1, e2]` are added to the goal state in this order.
 
 ```ocaml
 let cut c =
-  let open Sigma in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     (** In this block, we focus on one goal at a time indicated by gl *)
     let env = Proofview.Goal.env gl in
     (** Get the context of the goal, essentially [Γ] *)
@@ -80,25 +78,22 @@ let cut c =
     let t = mkArrow c (Vars.lift 1 concl) in
     (** Build [X -> A]. Note the lifting of [A] due to being on the right hand
         side of the arrow. *)
-    Refine.refine { run = begin fun sigma ->
+    Refine.refine begin fun sigma ->
       (** All evars generated by this block will be added as goals *)
-      let Sigma (f, sigma, p) = Evarutil.new_evar env sigma t in
+      let sigma, f = Evarutil.new_evar env sigma t in
       (** Generate ?e1 : [Γ ⊢ _ : X -> A], add it to sigma, and return the
           term [f := Γ ⊢ ?e1{Γ} : X -> A] with the updated sigma. The identity
           substitution for [Γ] is extracted from the [env] argument, so that
           one must be careful to pass the correct context here in order for the
           resulting term to be well-typed. The [p] return value is a proof term
           used to enforce sigma monotonicity. *)
-      let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c in
+      let sigma, x = Evarutil.new_evar env sigma c in
       (** Generate ?e2 : [Γ ⊢ _ : X] in sigma and return
           [x := Γ ⊢ ?e2{Γ} : X]. *)
       let r = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 r, [|mkRel 1|])) in
       (** Build [r := Γ ⊢ let id : X := ?e2{Γ} in ?e1{Γ} id : A] *)
-      Sigma (r, sigma, p +> q)
-      (** Fills the current hole with [r]. The [p +> q] thingy ensures
-          monotonicity of sigma. *)
-    end }
-  end }
+    end
+  end
 ```
 
 The `Evarutil.new_evar` function is the preferred way to generate evars in