Merge PR #12307: Cleaning up the legacy proof engine

Reviewed-by: ejgallego

11 files changed, 87 insertions, 134 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 0c305d09e8..c485c38009 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -290,7 +290,6 @@ let constr_of_term c = EConstr.of_constr (constr_of_term c)
 
 let rec proof_tac p : unit Proofview.tactic =
   Proofview.Goal.enter begin fun gl ->
-  try (* type_of can raise exceptions *)
   match p.p_rule with
       Ax c -> exact_check (EConstr.of_constr c)
     | SymAx c ->
@@ -350,7 +349,6 @@ let rec proof_tac p : unit Proofview.tactic =
            app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in
          Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
                                (Tacticals.New.tclTHEN injt (proof_tac prf))))
-  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end
 
 let refute_tac c t1 t2 p =
@@ -508,11 +506,9 @@ let f_equal =
     let concl = Proofview.Goal.concl gl in
     let sigma = Tacmach.New.project gl in
     let cut_eq c1 c2 =
-      try (* type_of can raise an exception *)
         Tacticals.New.tclTHENS
           (mk_eq _eq c1 c2 Tactics.cut)
           [Proofview.tclUNIT ();Tacticals.New.tclTRY ((app_global _refl_equal [||]) apply)]
-      with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
     in
     Proofview.tclORELSE
       begin match EConstr.kind sigma concl with
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 633cdbd735..e7c75e029e 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -690,15 +690,13 @@ let ring_lookup (f : Value.t) lH rl t =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
-    try (* find_ring_strucure can raise an exception *)
-      let rl = make_args_list sigma rl t in
-      let evdref = ref sigma in
-      let e = find_ring_structure env sigma rl in
-      let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in
-      let lH = carg (make_hyp_list env evdref lH) in
-      let ring = ltac_ring_structure e in
-      Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl]))
-    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+    let rl = make_args_list sigma rl t in
+    let evdref = ref sigma in
+    let e = find_ring_structure env sigma rl in
+    let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in
+    let lH = carg (make_hyp_list env evdref lH) in
+    let ring = ltac_ring_structure e in
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl]))
   end
 
 (***********************************************************************)
@@ -984,13 +982,11 @@ let field_lookup (f : Value.t) lH rl t =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
-    try
-      let rl = make_args_list sigma rl t in
-      let evdref = ref sigma in
-      let e = find_field_structure env sigma rl in
-      let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in
-      let lH = carg (make_hyp_list env evdref lH) in
-      let field = ltac_field_structure e in
-      Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl]))
-    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+    let rl = make_args_list sigma rl t in
+    let evdref = ref sigma in
+    let e = find_field_structure env sigma rl in
+    let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in
+    let lH = carg (make_hyp_list env evdref lH) in
+    let field = ltac_field_structure e in
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl]))
   end
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index c7110d7a91..e77c5082dd 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -614,7 +614,7 @@ let is_elim_predicate_explicitly_dependent env sigma pred indf =
 let set_names env sigma n brty =
   let open EConstr in
   let (ctxt,cl) = decompose_prod_n_assum sigma n brty in
-  EConstr.Unsafe.to_constr (Namegen.it_mkProd_or_LetIn_name env sigma cl ctxt)
+  Namegen.it_mkProd_or_LetIn_name env sigma cl ctxt
 
 let set_pattern_names env sigma ind brv =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
@@ -631,11 +631,12 @@ let type_case_branches_with_names env sigma indspec p c =
   let nparams = mib.mind_nparams in
   let (params,realargs) = List.chop nparams args in
   let lbrty = Inductive.build_branches_type ind specif params p in
+  let lbrty = Array.map EConstr.of_constr lbrty in
   (* Build case type *)
   let conclty = lambda_appvect_assum (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in
   (* Adjust names *)
   if is_elim_predicate_explicitly_dependent env sigma p (ind,params) then
-    (set_pattern_names env sigma (fst ind) (Array.map EConstr.of_constr lbrty), conclty)
+    (set_pattern_names env sigma (fst ind) lbrty, conclty)
   else (lbrty, conclty)
 
 (* Type of Case predicates *)
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index ab69629595..2bec86599e 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -194,7 +194,7 @@ val arity_of_case_predicate :
   env -> inductive_family -> bool -> Sorts.t -> types
 
 val type_case_branches_with_names :
-  env -> evar_map -> pinductive * EConstr.constr list -> constr -> constr -> types array * types
+  env -> evar_map -> pinductive * EConstr.constr list -> constr -> constr -> EConstr.types array * types
 
 (** Annotation for cases *)
 val make_case_info : env -> inductive -> Sorts.relevance -> case_style -> case_info
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 37d54a4eea..08178052bf 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -321,10 +321,6 @@ let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl =
     clenv_unify CUMUL ~flags
       (meta_reducible_instance clenv.evd clenv.templtyp) concl clenv
 
-let old_clenv_unique_resolver ?flags clenv gl =
-  let concl = Goal.V82.concl clenv.evd (sig_it gl) in
-  clenv_unique_resolver_gen ?flags clenv concl
-
 let clenv_unique_resolver ?flags clenv gl =
   let concl = Proofview.Goal.concl gl in
   clenv_unique_resolver_gen ?flags clenv concl
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 1adfdb885a..4279ab4768 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -63,9 +63,6 @@ val clenv_unify :
   ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
 
 (** unifies the concl of the goal with the type of the clenv *)
-val old_clenv_unique_resolver :
-  ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
-
 val clenv_unique_resolver :
   ?flags:unify_flags -> clausenv -> Proofview.Goal.t -> clausenv
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 695e103082..c5e341c720 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -13,7 +13,6 @@ open Constr
 open Termops
 open Evd
 open EConstr
-open Refiner
 open Logic
 open Reduction
 open Clenv
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 406e71aafc..c7a1c32e7c 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -28,16 +28,14 @@ module NamedDecl = Context.Named.Declaration
 type refiner_error =
 
   (* Errors raised by the refiner *)
-  | BadType of constr * constr * constr
+  | BadType of constr * constr * EConstr.t
   | UnresolvedBindings of Name.t list
   | CannotApply of constr * constr
-  | NotWellTyped of constr
   | NonLinearProof of constr
   | MetaInType of EConstr.constr
 
   (* Errors raised by the tactics *)
   | IntroNeedsProduct
-  | DoesNotOccurIn of constr * Id.t
   | NoSuchHyp of Id.t
 
 exception RefinerError of Environ.env * Evd.evar_map * refiner_error
@@ -73,13 +71,11 @@ let catchable_exception = function
 
 let error_no_such_hypothesis env sigma id = raise (RefinerError (env, sigma, NoSuchHyp id))
 
-(* Tells if the refiner should check that the submitted rules do not
-   produce invalid subgoals *)
-let check = ref false
-let with_check = Flags.with_option check
+(* The check flag tells if the refiner should check that the submitted rules do
+   not produce invalid subgoals *)
 
-let check_typability env sigma c =
-  if !check then fst (type_of env sigma (EConstr.of_constr c)) else sigma
+let check_typability ~check env sigma c =
+  if check then fst (type_of env sigma (EConstr.of_constr c)) else sigma
 
 (************************************************************************)
 (************************************************************************)
@@ -316,9 +312,9 @@ let check_meta_variables env sigma c =
   if not (List.distinct_f Int.compare (collect_meta_variables c)) then
     raise (RefinerError (env, sigma, NonLinearProof c))
 
-let check_conv_leq_goal env sigma arg ty conclty =
-  if !check then
-    let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
+let check_conv_leq_goal ~check env sigma arg ty conclty =
+  if check then
+    let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) conclty in
     match ans with
     | Some evm -> evm
     | None -> raise (RefinerError (env, sigma, BadType (arg,ty,conclty)))
@@ -334,28 +330,27 @@ let meta_free_prefix sigma a =
     in a
   with Stop acc -> Array.rev_of_list acc
 
-let goal_type_of env sigma c =
-  if !check then
+let goal_type_of ~check env sigma c =
+  if check then
     let (sigma,t) = type_of env sigma (EConstr.of_constr c) in
     (sigma, EConstr.Unsafe.to_constr t)
   else (sigma, EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c)))
 
-let rec mk_refgoals sigma goal goalacc conclty trm =
-  let env = Goal.V82.env sigma goal in
-  let hyps = Goal.V82.hyps sigma goal in
+let rec mk_refgoals ~check env sigma goalacc conclty trm =
+  let hyps = Environ.named_context_val env in
   let mk_goal hyps concl =
     Goal.V82.mk_goal sigma hyps concl
   in
-    if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then
+    if (not check) && not (occur_meta sigma (EConstr.of_constr trm)) then
       let t'ty = Retyping.get_type_of env sigma (EConstr.of_constr trm) in
       let t'ty = EConstr.Unsafe.to_constr t'ty in
-      let sigma = check_conv_leq_goal env sigma trm t'ty conclty in
+      let sigma = check_conv_leq_goal ~check env sigma trm t'ty conclty in
         (goalacc,t'ty,sigma,trm)
     else
       match kind trm with
       | Meta _ ->
-        let conclty = nf_betaiota env sigma (EConstr.of_constr conclty) in
-          if !check && occur_meta sigma conclty then
+        let conclty = nf_betaiota env sigma conclty in
+          if check && occur_meta sigma conclty then
             raise (RefinerError (env, sigma, MetaInType conclty));
           let (gl,ev,sigma) = mk_goal hyps conclty in
           let ev = EConstr.Unsafe.to_constr ev in
@@ -363,9 +358,9 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
           gl::goalacc, conclty, sigma, ev
 
       | Cast (t,k, ty) ->
-        let sigma = check_typability env sigma ty in
-        let sigma = check_conv_leq_goal env sigma trm ty conclty in
-        let res = mk_refgoals sigma goal goalacc ty t in
+        let sigma = check_typability ~check env sigma ty in
+        let sigma = check_conv_leq_goal ~check env sigma trm ty conclty in
+        let res = mk_refgoals ~check env sigma goalacc (EConstr.of_constr ty) t in
         (* we keep the casts (in particular VMcast and NATIVEcast) except
            when they are annotating metas *)
         if isMeta t then begin
@@ -388,24 +383,24 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
             let ty = EConstr.Unsafe.to_constr ty in
               goalacc, ty, sigma, f
           else
-            mk_hdgoals sigma goal goalacc f
+            mk_hdgoals ~check env sigma goalacc f
         in
-        let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in
-        let sigma = check_conv_leq_goal env sigma trm conclty' conclty in
+        let ((acc'',conclty',sigma), args) = mk_arggoals ~check env sigma acc' hdty l in
+        let sigma = check_conv_leq_goal ~check env sigma trm conclty' conclty in
         let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in
         (acc'',conclty',sigma, ans)
 
       | Proj (p,c) ->
-        let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in
+        let (acc',cty,sigma,c') = mk_hdgoals ~check env sigma goalacc c in
         let c = mkProj (p, c') in
         let ty = get_type_of env sigma (EConstr.of_constr c) in
         let ty = EConstr.Unsafe.to_constr ty in
           (acc',ty,sigma,c)
 
       | Case (ci,p,c,lf) ->
-        let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
-        let sigma = check_conv_leq_goal env sigma trm conclty' conclty in
-        let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in
+        let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals ~check env sigma goalacc p c in
+        let sigma = check_conv_leq_goal ~check env sigma trm conclty' conclty in
+        let (acc'',sigma,rbranches) = treat_case ~check env sigma ci lbrty lf acc' in
         let lf' = Array.rev_of_list rbranches in
         let ans =
           if p' == p && c' == c && Array.equal (==) lf' lf then trm
@@ -416,28 +411,27 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
       | _ ->
         if occur_meta sigma (EConstr.of_constr trm) then
           anomaly (Pp.str "refiner called with a meta in non app/case subterm.");
-        let (sigma, t'ty) = goal_type_of env sigma trm in
-        let sigma = check_conv_leq_goal env sigma trm t'ty conclty in
+        let (sigma, t'ty) = goal_type_of ~check env sigma trm in
+        let sigma = check_conv_leq_goal ~check env sigma trm t'ty conclty in
           (goalacc,t'ty,sigma, trm)
 
 (* Same as mkREFGOALS but without knowing the type of the term. Therefore,
  * Metas should be casted. *)
 
-and mk_hdgoals sigma goal goalacc trm =
-  let env = Goal.V82.env sigma goal in
-  let hyps = Goal.V82.hyps sigma goal in
+and mk_hdgoals ~check env sigma goalacc trm =
+  let hyps = Environ.named_context_val env in
   let mk_goal hyps concl =
     Goal.V82.mk_goal sigma hyps concl in
   match kind trm with
     | Cast (c,_, ty) when isMeta c ->
-        let sigma = check_typability env sigma ty in
+        let sigma = check_typability ~check env sigma ty in
         let (gl,ev,sigma) = mk_goal hyps (nf_betaiota env sigma (EConstr.of_constr ty)) in
         let ev = EConstr.Unsafe.to_constr ev in
         gl::goalacc,ty,sigma,ev
 
     | Cast (t,_, ty) ->
-        let sigma = check_typability env sigma ty in
-        mk_refgoals sigma goal goalacc ty t
+        let sigma = check_typability ~check env sigma ty in
+        mk_refgoals ~check env sigma goalacc (EConstr.of_constr ty) t
 
     | App (f,l) ->
         let (acc',hdty,sigma,applicand) =
@@ -445,15 +439,15 @@ and mk_hdgoals sigma goal goalacc trm =
           then
             let l' = meta_free_prefix sigma l in
            (goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f)
-          else mk_hdgoals sigma goal goalacc f
+          else mk_hdgoals ~check env sigma goalacc f
         in
-        let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in
+        let ((acc'',conclty',sigma), args) = mk_arggoals ~check env sigma acc' hdty l in
         let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in
         (acc'',conclty',sigma, ans)
 
     | Case (ci,p,c,lf) ->
-        let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
-        let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in
+        let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals ~check env sigma goalacc p c in
+        let (acc'',sigma,rbranches) = treat_case ~check env sigma ci lbrty lf acc' in
         let lf' = Array.rev_of_list rbranches in
         let ans =
           if p' == p && c' == c && Array.equal (==) lf' lf then trm
@@ -462,21 +456,21 @@ and mk_hdgoals sigma goal goalacc trm =
         (acc'',conclty',sigma, ans)
 
     | Proj (p,c) ->
-         let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in
+         let (acc',cty,sigma,c') = mk_hdgoals ~check env sigma goalacc c in
          let c = mkProj (p, c') in
          let ty = get_type_of env sigma (EConstr.of_constr c) in
          let ty = EConstr.Unsafe.to_constr ty in
            (acc',ty,sigma,c)
 
     | _ ->
-        if !check && occur_meta sigma (EConstr.of_constr trm) then
+        if check && occur_meta sigma (EConstr.of_constr trm) then
           anomaly (Pp.str "refine called with a dependent meta.");
-        let (sigma, ty) = goal_type_of env sigma trm in
+        let (sigma, ty) = goal_type_of env ~check sigma trm in
         goalacc, ty, sigma, trm
 
-and mk_arggoals sigma goal goalacc funty allargs =
+and mk_arggoals ~check env sigma goalacc funty allargs =
   let foldmap (goalacc, funty, sigma) harg =
-    let t = whd_all (Goal.V82.env sigma goal) sigma (EConstr.of_constr funty) in
+    let t = whd_all env sigma (EConstr.of_constr funty) in
     let t = EConstr.Unsafe.to_constr t in
     let rec collapse t = match kind t with
     | LetIn (_, c1, _, b) -> collapse (subst1 c1 b)
@@ -485,19 +479,17 @@ and mk_arggoals sigma goal goalacc funty allargs =
     let t = collapse t in
     match kind t with
     | Prod (_, c1, b) ->
-      let (acc, hargty, sigma, arg) = mk_refgoals sigma goal goalacc c1 harg in
+      let (acc, hargty, sigma, arg) = mk_refgoals ~check env sigma goalacc (EConstr.of_constr c1) harg in
       (acc, subst1 harg b, sigma), arg
     | _ ->
-      let env = Goal.V82.env sigma goal in
       raise (RefinerError (env,sigma,CannotApply (t, harg)))
   in
   Array.Smart.fold_left_map foldmap (goalacc, funty, sigma) allargs
 
-and mk_casegoals sigma goal goalacc p c =
-  let env = Goal.V82.env sigma goal in
-  let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in
+and mk_casegoals ~check env sigma goalacc p c =
+  let (acc',ct,sigma,c') = mk_hdgoals ~check env sigma goalacc c in
   let ct = EConstr.of_constr ct in
-  let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in
+  let (acc'',pt,sigma,p') = mk_hdgoals ~check env sigma acc' p in
   let ((ind, u), spec) =
     try Tacred.find_hnf_rectype env sigma ct
     with Not_found -> anomaly (Pp.str "mk_casegoals.") in
@@ -505,20 +497,19 @@ and mk_casegoals sigma goal goalacc p c =
   let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in
   (acc'',lbrty,conclty,sigma,p',c')
 
-and treat_case sigma goal ci lbrty lf acc' =
+and treat_case ~check env sigma ci lbrty lf acc' =
   let rec strip_outer_cast c = match kind c with
   | Cast (c,_,_) -> strip_outer_cast c
   | _ -> c in
   let decompose_app_vect c = match kind c with
   | App (f,cl) -> (f, cl)
   | _ -> (c,[||]) in
-  let env = Goal.V82.env sigma goal in
   Array.fold_left3
     (fun (lacc,sigma,bacc) ty fi l ->
         if isMeta (strip_outer_cast fi) then
           (* Support for non-eta-let-expanded Meta as found in *)
           (* destruct/case with an non eta-let expanded elimination scheme *)
-          let (r,_,s,fi') = mk_refgoals sigma goal lacc ty fi in
+          let (r,_,s,fi') = mk_refgoals ~check env sigma lacc ty fi in
           r,s,(fi'::bacc)
         else
         (* Deal with a branch in expanded form of the form
@@ -539,14 +530,14 @@ and treat_case sigma goal ci lbrty lf acc' =
         if isMeta head then begin
           assert (args = Context.Rel.to_extended_vect mkRel 0 ctx);
           let head' = lift (-n) head in
-          let (r,_,s,head'') = mk_refgoals sigma goal lacc ty head' in
+          let (r,_,s,head'') = mk_refgoals ~check env sigma lacc ty head' in
           let fi' = it_mkLambda_or_LetIn (mkApp (head'',args)) ctx in
           (r,s,fi'::bacc)
         end
         else
           (* Supposed to be meta-free *)
-          let sigma, t'ty = goal_type_of env sigma fi in
-          let sigma = check_conv_leq_goal env sigma fi t'ty ty in
+          let sigma, t'ty = goal_type_of ~check env sigma fi in
+          let sigma = check_conv_leq_goal ~check env sigma fi t'ty ty in
           (lacc,sigma,fi::bacc))
     (acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags
 
@@ -574,18 +565,18 @@ let convert_hyp ~check ~reorder env sigma d =
 (************************************************************************)
 (* Primitive tactics are handled here *)
 
-let prim_refiner r sigma goal =
-  let env = Goal.V82.env sigma goal in
-  let cl = Goal.V82.concl sigma goal in
-  let cl = EConstr.Unsafe.to_constr cl in
+let refiner ~check r =
+  let open Proofview.Notations in
+  Proofview.Goal.enter begin fun gl ->
+  let sigma = Proofview.Goal.sigma gl in
+  let env = Proofview.Goal.env gl in
+  let st = Proofview.Goal.state gl in
+  let cl = Proofview.Goal.concl gl in
   check_meta_variables env sigma r;
-  let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl r in
-  let sgl = List.rev sgl in
-  let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in
-  (sgl, sigma)
-
-let prim_refiner ~check r sigma goal =
-  if check then
-    with_check (prim_refiner r sigma) goal
-  else
-    prim_refiner r sigma goal
+  let (sgl,cl',sigma,oterm) = mk_refgoals ~check env sigma [] cl r in
+  let map gl = Proofview.goal_with_state gl st in
+  let sgl = List.rev_map map sgl in
+  let sigma = Goal.V82.partial_solution env sigma (Proofview.Goal.goal gl) (EConstr.of_constr oterm) in
+  Proofview.Unsafe.tclEVARS sigma <*>
+  Proofview.Unsafe.tclSETGOALS sgl
+  end
diff --git a/proofs/logic.mli b/proofs/logic.mli
index ef8b2731b2..9dc75000a1 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -26,23 +26,21 @@ open Evd
 
 (** The primitive refiner. *)
 
-val prim_refiner : check:bool -> constr -> evar_map -> Goal.goal -> Goal.goal list * evar_map
+val refiner : check:bool -> constr -> unit Proofview.tactic
 
 (** {6 Refiner errors. } *)
 
 type refiner_error =
 
   (*i Errors raised by the refiner i*)
-  | BadType of constr * constr * constr
+  | BadType of constr * constr * EConstr.t
   | UnresolvedBindings of Name.t list
   | CannotApply of constr * constr
-  | NotWellTyped of constr
   | NonLinearProof of constr
   | MetaInType of EConstr.constr
 
   (*i Errors raised by the tactics i*)
   | IntroNeedsProduct
-  | DoesNotOccurIn of constr * Id.t
   | NoSuchHyp of Id.t
 
 exception RefinerError of Environ.env * evar_map * refiner_error
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 29a47c5acd..874bab277d 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -12,7 +12,6 @@ open Pp
 open CErrors
 open Util
 open Evd
-open Logic
 
 type tactic = Proofview.V82.tac
 
@@ -26,18 +25,7 @@ let project x = x.sigma
 let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls))
 let pf_hyps gls = EConstr.named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls))
 
-let refiner ~check pr goal_sigma =
-  let (sgl,sigma') = prim_refiner ~check pr goal_sigma.sigma goal_sigma.it in
-  { it = sgl; sigma = sigma'; }
-
-(* Profiling refiner *)
-let refiner ~check =
-  if Flags.profile then
-    let refiner_key = CProfile.declare_profile "refiner" in
-      CProfile.profile2 refiner_key (refiner ~check)
-  else refiner ~check
-
-let refiner ~check c = Proofview.V82.tactic ~nf_evars:false (refiner ~check c)
+let refiner = Logic.refiner
 
 (*********************)
 (*   Tacticals       *)
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 41f2ab9c63..9d67ce3757 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1096,7 +1096,7 @@ let explain_typeclass_error env sigma = function
 (* Refiner errors *)
 
 let explain_refiner_bad_type env sigma arg ty conclty =
-  let pm, pn = with_diffs (pr_lconstr_env env sigma ty) (pr_lconstr_env env sigma conclty) in
+  let pm, pn = with_diffs (pr_lconstr_env env sigma ty) (pr_leconstr_env env sigma conclty) in
   str "Refiner was given an argument" ++ brk(1,1) ++
   pr_lconstr_env env sigma arg ++ spc () ++
   str "of type" ++ brk(1,1) ++ pm ++ spc () ++
@@ -1112,16 +1112,9 @@ let explain_refiner_cannot_apply env sigma t harg =
   pr_lconstr_env env sigma t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++
   pr_lconstr_env env sigma harg ++ str "."
 
-let explain_refiner_not_well_typed env sigma c =
-  str "The term " ++ pr_lconstr_env env sigma c ++ str " is not well-typed."
-
 let explain_intro_needs_product () =
   str "Introduction tactics needs products."
 
-let explain_does_not_occur_in env sigma c hyp =
-  str "The term" ++ spc () ++ pr_lconstr_env env sigma c ++ spc () ++
-  str "does not occur in" ++ spc () ++ Id.print hyp ++ str "."
-
 let explain_non_linear_proof env sigma c =
   str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr_env env sigma c ++
   spc () ++ str "because a metavariable has several occurrences."
@@ -1137,9 +1130,7 @@ let explain_refiner_error env sigma = function
   | BadType (arg,ty,conclty) -> explain_refiner_bad_type env sigma arg ty conclty
   | UnresolvedBindings t -> explain_refiner_unresolved_bindings t
   | CannotApply (t,harg) -> explain_refiner_cannot_apply env sigma t harg
-  | NotWellTyped c -> explain_refiner_not_well_typed env sigma c
   | IntroNeedsProduct -> explain_intro_needs_product ()
-  | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in env sigma c hyp
   | NonLinearProof c -> explain_non_linear_proof env sigma c
   | MetaInType c -> explain_meta_in_type env sigma c
   | NoSuchHyp id -> explain_no_such_hyp id