Moving the lowest parts of pretyping/ (Evarutil & Proofview) to engine/.

Some functions exported by Evarutil essentially used by the unification
engine were moved to a new file Evardefine. Their presence in Evarutil was
not making much sense.

Moreover, the Refine module of the Proofview file was turned into a proper
file in pretyping/. This is because this part of the code was relying on
the typing primitives from Pretyping.

6 files changed, 29 insertions, 25 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 0cc796886c..23aa8dcb47 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -370,7 +370,7 @@ let refine_tac ist simple c =
     let expected_type = Pretyping.OfType concl in
     let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in
     let update = { run = fun sigma -> c.delayed env sigma } in
-    let refine = Proofview.Refine.refine ~unsafe:false update in
+    let refine = Refine.refine ~unsafe:false update in
     if simple then refine
     else refine <*>
            Tactics.New.reduce_after_refine <*>
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 730da147af..e5abad6863 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1072,7 +1072,7 @@ let prepare_hint check (poly,local) env init (sigma,c) =
       subst := (evar,mkVar id)::!subst;
       mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in
   let c' = iter c in
-    if check then Evarutil.check_evars (Global.env()) Evd.empty sigma c';
+    if check then Pretyping.check_evars (Global.env()) Evd.empty sigma c';
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
     if poly then IsConstr (c', diff)
     else if local then IsConstr (c', diff)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 6841ab0ecd..89c6beb321 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -459,7 +459,7 @@ let raw_inversion inv_kind id status names =
     in
     let refined id =
       let prf = mkApp (mkVar id, args) in
-      Proofview.Refine.refine { run = fun h -> Sigma (prf, h, Sigma.refl) }
+      Refine.refine { run = fun h -> Sigma (prf, h, Sigma.refl) }
     in
     let neqns = List.length realargs in
     let as_mode = names != None in
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 67d21886b2..fb04bee070 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1539,7 +1539,7 @@ let assert_replacing id newt tac =
     | d :: rem -> insert_dependent env (LocalAssum (get_id d, newt)) [] after @ rem
     in
     let env' = Environ.reset_with_named_context (val_of_named_context nc) env in
-    Proofview.Refine.refine ~unsafe:false { run = begin fun sigma ->
+    Refine.refine ~unsafe:false { run = begin fun sigma ->
       let Sigma (ev, sigma, p) = Evarutil.new_evar env' sigma concl in
       let Sigma (ev', sigma, q) = Evarutil.new_evar env sigma newt in
       let map d =
@@ -1568,7 +1568,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
         let gls = List.rev (Evd.fold_undefined fold undef []) in
 	match clause, prf with
 	| Some id, Some p ->
-            let tac = Proofview.Refine.refine ~unsafe:false { run = fun h -> Sigma (p, h, Sigma.refl) } <*> Proofview.Unsafe.tclNEWGOALS gls in
+            let tac = Refine.refine ~unsafe:false { run = fun h -> Sigma (p, h, Sigma.refl) } <*> Proofview.Unsafe.tclNEWGOALS gls in
             Proofview.Unsafe.tclEVARS undef <*>
 	    assert_replacing id newt tac
 	| Some id, None ->
@@ -1582,7 +1582,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
               let Sigma (ev, sigma, q) = Evarutil.new_evar env sigma newt in
               Sigma (mkApp (p, [| ev |]), sigma, q)
             end } in
-            Proofview.Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls
+            Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls
             end }
 	| None, None ->
             Proofview.Unsafe.tclEVARS undef <*>
@@ -1880,7 +1880,7 @@ let build_morphism_signature m =
   let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in
   let evd = solve_constraints env !evd in
   let m = Evarutil.nf_evar evd morph in
-    Evarutil.check_evars env Evd.empty evd m; m
+    Pretyping.check_evars env Evd.empty evd m; m
 
 let default_morphism sign m =
   let env = Global.env () in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f725a06549..7ae178af57 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -163,7 +163,7 @@ let _ =
     does not check anything. *)
 let unsafe_intro env store decl b =
   let open Context.Named.Declaration in
-  Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+  Refine.refine ~unsafe:true { run = begin fun sigma ->
     let ctx = named_context_val env in
     let nctx = push_named_context_val decl ctx in
     let inst = List.map (mkVar % get_id) (named_context env) in
@@ -199,7 +199,7 @@ let convert_concl ?(check=true) ty k =
     let env = Proofview.Goal.env gl in
     let store = Proofview.Goal.extra gl in
     let conclty = Proofview.Goal.raw_concl gl in
-    Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+    Refine.refine ~unsafe:true { run = begin fun sigma ->
       let Sigma ((), sigma, p) =
         if check then begin
           let sigma = Sigma.to_evar_map sigma in
@@ -222,7 +222,7 @@ let convert_hyp ?(check=true) d =
     let store = Proofview.Goal.extra gl in
     let sign = convert_hyp check (named_context_val env) sigma d in
     let env = reset_with_named_context sign env in
-    Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+    Refine.refine ~unsafe:true { run = begin fun sigma ->
       Evarutil.new_evar env sigma ~principal:true ~store ty
     end }
   end }
@@ -345,7 +345,7 @@ let rename_hyp repl =
       let nconcl = subst concl in
       let nctx = Environ.val_of_named_context nhyps in
       let instance = List.map (mkVar % get_id) hyps in
-      Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+      Refine.refine ~unsafe:true { run = begin fun sigma ->
         Evarutil.new_evar_instance nctx sigma nconcl ~store instance
       end }
     end }
@@ -1070,7 +1070,7 @@ let cut c =
       let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_of_hyps gl) in
       (** Backward compat: normalize [c]. *)
       let c = if normalize_cut then local_strong whd_betaiota sigma c else c in
-      Proofview.Refine.refine ~unsafe:true { run = begin fun h ->
+      Refine.refine ~unsafe:true { run = begin fun h ->
         let Sigma (f, h, p) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in
         let Sigma (x, h, q) = Evarutil.new_evar env h c in
         let f = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in
@@ -1736,7 +1736,7 @@ let cut_and_apply c =
       | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
         let concl = Proofview.Goal.concl gl in
         let env = Tacmach.New.pf_env gl in
-        Proofview.Refine.refine { run = begin fun sigma ->
+        Refine.refine { run = begin fun sigma ->
           let typ = mkProd (Anonymous, c2, concl) in
           let Sigma (f, sigma, p) = Evarutil.new_evar env sigma typ in
           let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c1 in
@@ -1757,7 +1757,7 @@ let cut_and_apply c =
 (* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *)
 
 let new_exact_no_check c =
-  Proofview.Refine.refine ~unsafe:true { run = fun h -> Sigma.here c h }
+  Refine.refine ~unsafe:true { run = fun h -> Sigma.here c h }
 
 let exact_check c =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
@@ -1808,7 +1808,7 @@ let assumption =
     in
     if is_same_type then
       (Proofview.Unsafe.tclEVARS sigma) <*>
-	Proofview.Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar (get_id decl)) h }
+	Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar (get_id decl)) h }
     else arec gl only_eq rest
   in
   let assumption_tac = { enter = begin fun gl ->
@@ -1893,7 +1893,7 @@ let clear_body ids =
       check_is_type env concl msg
     in
     check_hyps <*> check_concl <*>
-    Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+    Refine.refine ~unsafe:true { run = begin fun sigma ->
       Evarutil.new_evar env sigma ~principal:true concl
     end }
   end }
@@ -1950,7 +1950,7 @@ let apply_type newcl args =
   Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
     let store = Proofview.Goal.extra gl in
-    Proofview.Refine.refine { run = begin fun sigma ->
+    Refine.refine { run = begin fun sigma ->
       let newcl = nf_betaiota (Sigma.to_evar_map sigma) newcl (* As in former Logic.refine *) in
       let Sigma (ev, sigma, p) =
         Evarutil.new_evar env sigma ~principal:true ~store newcl in
@@ -1971,7 +1971,7 @@ let bring_hyps hyps =
       let concl = Tacmach.New.pf_nf_concl gl in
       let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
       let args = Array.of_list (Context.Named.to_instance hyps) in
-      Proofview.Refine.refine { run = begin fun sigma ->
+      Refine.refine { run = begin fun sigma ->
         let Sigma (ev, sigma, p) =
           Evarutil.new_evar env sigma ~principal:true ~store newcl in
         Sigma (mkApp (ev, args), sigma, p)
@@ -2671,7 +2671,7 @@ let new_generalize_gen_let lconstr =
 	0 lconstr (concl, sigma, [])
     in
     let tac =
-	Proofview.Refine.refine { run = begin fun sigma ->
+	Refine.refine { run = begin fun sigma ->
           let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma ~principal:true newcl in
           Sigma ((applist (ev, args)), sigma, p)
 	end }
@@ -3325,7 +3325,7 @@ let mk_term_eq env sigma ty t ty' t' =
 
 let make_abstract_generalize env id typ concl dep ctx body c eqs args refls =
   let open Context.Rel.Declaration in
-  Proofview.Refine.refine { run = begin fun sigma ->
+  Refine.refine { run = begin fun sigma ->
   let eqslen = List.length eqs in
     (* Abstract by the "generalized" hypothesis equality proof if necessary. *)
   let abshypeq, abshypt =
@@ -4095,6 +4095,10 @@ let check_enough_applied env sigma elim =
           (* Last argument is supposed to be the induction argument *)
           check_expected_type env sigma elimc elimt
 
+let guard_no_unifiable = Proofview.guard_no_unifiable >>= function
+| None -> Proofview.tclUNIT ()
+| Some l -> Proofview.tclZERO (RefinerError (UnresolvedBindings l))
+
 let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
      id ((pending,(c0,lbind)),(eqname,names)) t0 inhyps cls tac =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
@@ -4122,14 +4126,14 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
           (* and destruct has side conditions first *)
           Tacticals.New.tclTHENLAST)
       (Tacticals.New.tclTHENLIST [
-        Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+        Refine.refine ~unsafe:true { run = begin fun sigma ->
           let b = not with_evars && with_eq != None in
           let Sigma (c, sigma, p) = use_bindings env sigma elim b (c0,lbind) t0 in
           let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in
           let Sigma (ans, sigma, q) = mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t) in
           Sigma (ans, sigma, p +> q)
         end };
-        Proofview.(if with_evars then shelve_unifiable else guard_no_unifiable);
+        if with_evars then Proofview.shelve_unifiable else guard_no_unifiable;
         if is_arg_pure_hyp
         then Tacticals.New.tclTRY (Proofview.V82.tactic (thin [destVar c0]))
         else Proofview.tclUNIT ();
@@ -4146,7 +4150,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
       let env = reset_with_named_context sign env in
       let tac =
       Tacticals.New.tclTHENLIST [
-        Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+        Refine.refine ~unsafe:true { run = begin fun sigma ->
           mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None
         end };
         tac
@@ -4791,6 +4795,6 @@ module New = struct
       {onhyps=None; concl_occs=AllOccurrences }
 
   let refine ?unsafe c =
-    Proofview.Refine.refine ?unsafe c <*>
+    Refine.refine ?unsafe c <*>
     reduce_after_refine
 end
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 26ea017696..4c4a96ec07 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -431,7 +431,7 @@ end
 module New : sig
 
   val refine : ?unsafe:bool -> constr Sigma.run -> unit Proofview.tactic
-  (** [refine ?unsafe c] is [Proofview.Refine.refine ?unsafe c]
+  (** [refine ?unsafe c] is [Refine.refine ?unsafe c]
       followed by beta-iota-reduction of the conclusion. *)
 
   val reduce_after_refine : unit Proofview.tactic