1 files changed, 63 insertions, 40 deletions

diff --git a/proofs/refine.ml b/proofs/refine.ml
index 3f552706..909556b1 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -1,16 +1,19 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Util
-open Sigma.Notations
 open Proofview.Notations
 open Context.Named.Declaration
 
+module NamedDecl = Context.Named.Declaration
+
 let extract_prefix env info =
   let ctx1 = List.rev (Environ.named_context env) in
   let ctx2 = List.rev (Evd.evar_context info) in
@@ -26,12 +29,12 @@ let typecheck_evar ev env sigma =
   let info = Evd.find sigma ev in
   (** Typecheck the hypotheses. *)
   let type_hyp (sigma, env) decl =
-    let t = get_type decl in
+    let t = EConstr.of_constr (NamedDecl.get_type decl) in
     let evdref = ref sigma in
     let _ = Typing.e_sort_of env evdref t in
     let () = match decl with
     | LocalAssum _ -> ()
-    | LocalDef (_,body,_) -> Typing.e_check env evdref body t
+    | LocalDef (_,body,_) -> Typing.e_check env evdref (EConstr.of_constr body) t
     in
     (!evdref, Environ.push_named decl env)
   in
@@ -40,7 +43,7 @@ let typecheck_evar ev env sigma =
   let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
   (** Typecheck the conclusion *)
   let evdref = ref sigma in
-  let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in
+  let _ = Typing.e_sort_of env evdref (EConstr.of_constr (Evd.evar_concl info)) in
   !evdref
 
 let typecheck_proof c concl env sigma =
@@ -68,38 +71,48 @@ let add_side_effect env = function
 let add_side_effects env effects =
   List.fold_left (fun env eff -> add_side_effect env eff) env effects
 
-let make_refine_enter ?(unsafe = true) f =
-  { enter = fun gl ->
-  let gl = Proofview.Goal.assume gl in
+let generic_refine ~typecheck f gl =
   let sigma = Proofview.Goal.sigma gl in
-  let sigma = Sigma.to_evar_map sigma in
   let env = Proofview.Goal.env gl in
   let concl = Proofview.Goal.concl gl in
+  let state = Proofview.Goal.state gl in
   (** Save the [future_goals] state to restore them after the
       refinement. *)
-  let prev_future_goals = Evd.future_goals sigma in
-  let prev_principal_goal = Evd.principal_future_goal sigma in
+  let prev_future_goals = Evd.save_future_goals sigma in
   (** Create the refinement term *)
-  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
+  Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () ->
+  f >>= fun (v, c) ->
+  Proofview.tclEVARMAP >>= fun sigma ->
+  Proofview.V82.wrap_exceptions begin fun () ->
+  let evs = Evd.save_future_goals sigma in
   (** Redo the effects in sigma in the monad's env *)
   let privates_csts = Evd.eval_side_effects sigma in
   let sideff = Safe_typing.side_effects_of_private_constants privates_csts in
   let env = add_side_effects env sideff in
   (** Check that the introduced evars are well-typed *)
   let fold accu ev = typecheck_evar ev env accu in
-  let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in
+  let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in
   (** Check that the refined term is typesafe *)
-  let sigma = if unsafe then sigma else typecheck_proof c concl env sigma in
+  let sigma = if typecheck then typecheck_proof c concl env sigma else sigma in
   (** Check that the goal itself does not appear in the refined term *)
   let self = Proofview.Goal.goal gl in
   let _ =
     if not (Evarutil.occur_evar_upto sigma self c) then ()
     else Pretype_errors.error_occur_check env sigma self c
   in
+  (** Restore the [future goals] state. *)
+  let sigma = Evd.restore_future_goals sigma prev_future_goals in
+  (** Select the goals *)
+  let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) evs in
+  let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in
   (** Proceed to the refinement *)
-  let sigma = match evkmain with
+  let c = EConstr.Unsafe.to_constr c in
+  let sigma = match Proofview.Unsafe.advance sigma self with
+  | None ->
+    (** Nothing to do, the goal has been solved by side-effect *)
+    sigma
+  | Some self ->
+    match evkmain with
     | None -> Evd.define self c sigma
     | Some evk ->
         let id = Evd.evar_ident self sigma in
@@ -108,25 +121,37 @@ let make_refine_enter ?(unsafe = true) f =
         | None -> sigma
         | Some id -> Evd.rename evk id sigma
   in
-  (** Restore the [future goals] state. *)
-  let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in
-  (** Select the goals *)
-  let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in
+  (** Mark goals *)
   let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in
+  let comb = CList.map (fun x -> Proofview.goal_with_state x state) 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 v) >>= fun v ->
   Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*>
   Proofview.Unsafe.tclEVARS sigma <*>
   Proofview.Unsafe.tclSETGOALS comb <*>
+  Proofview.Unsafe.tclPUTSHELF shelf <*>
+  Proofview.Unsafe.tclPUTGIVENUP given_up <*>
   Proofview.tclUNIT v
-  }
+  end
 
-let refine_one ?(unsafe = true) f =
-  Proofview.Goal.enter_one (make_refine_enter ~unsafe f)
+let lift c =
+  Proofview.tclEVARMAP >>= fun sigma ->
+  Proofview.V82.wrap_exceptions begin fun () ->
+  let (sigma, c) = c sigma in
+  Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+  Proofview.tclUNIT c
+  end
 
-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)
+let make_refine_enter ~typecheck f gl = generic_refine ~typecheck (lift f) gl
+
+let refine_one ~typecheck f =
+  Proofview.Goal.enter_one (make_refine_enter ~typecheck f)
+
+let refine ~typecheck f =
+  let f evd =
+    let (evd,c) = f evd in (evd,((), c))
+  in
+  Proofview.Goal.enter (make_refine_enter ~typecheck f)
 
 (** Useful definitions *)
 
@@ -134,21 +159,19 @@ let with_type env evd c t =
   let my_type = Retyping.get_type_of env evd c in
   let j = Environ.make_judge c my_type in
   let (evd,j') =
-    Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t
+    Coercion.inh_conv_coerce_to true env evd j t
   in
   evd , j'.Environ.uj_val
 
-let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl ->
-  let gl = Proofview.Goal.assume gl in
+let refine_casted ~typecheck f = Proofview.Goal.enter begin fun gl ->
   let concl = Proofview.Goal.concl gl in
   let env = Proofview.Goal.env gl in
-  let f = { run = fun h ->
-    let Sigma (c, h, p) = f.run h in
-    let sigma, c = with_type env (Sigma.to_evar_map h) c concl in
-    Sigma (c, Sigma.Unsafe.of_evar_map sigma, p)
-  } in
-  refine ?unsafe f
-end }
+  let f h =
+    let (h, c) = f h in
+    with_type env h c concl
+  in
+  refine ~typecheck f
+end
 
 (** {7 solve_constraints}