From e802f48faf7a472000e218c7a3321c10c2171e0f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 12 May 2020 11:50:45 +0200
Subject: Remove useless try-with blocks in congruence.

The inner body was not raising any exception since it was in the monad,
and even if it did so, the enter block would have caught it.
---
 plugins/cc/cctac.ml | 4 ----
 1 file changed, 4 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
-- 
cgit v1.2.3


From d31cb4d3e55da99d42abdc1f4129ddc03e1631c6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 12 May 2020 12:02:23 +0200
Subject: Do not use Unsafe.to_constr for old refiner conclusion.

This was useless, since we did not observe the difference on evars.
---
 pretyping/inductiveops.ml  |  5 +++--
 pretyping/inductiveops.mli |  2 +-
 proofs/logic.ml            | 13 ++++++-------
 proofs/logic.mli           |  2 +-
 vernac/himsg.ml            |  2 +-
 5 files changed, 12 insertions(+), 12 deletions(-)

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/logic.ml b/proofs/logic.ml
index 406e71aafc..4eb8658f83 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -28,7 +28,7 @@ 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
@@ -318,7 +318,7 @@ let check_meta_variables env sigma 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 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)))
@@ -354,7 +354,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
     else
       match kind trm with
       | Meta _ ->
-        let conclty = nf_betaiota env sigma (EConstr.of_constr conclty) in
+        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
@@ -365,7 +365,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
       | 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 res = mk_refgoals sigma goal 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
@@ -437,7 +437,7 @@ and mk_hdgoals sigma goal goalacc trm =
 
     | Cast (t,_, ty) ->
         let sigma = check_typability env sigma ty in
-        mk_refgoals sigma goal goalacc ty t
+        mk_refgoals sigma goal goalacc (EConstr.of_constr ty) t
 
     | App (f,l) ->
         let (acc',hdty,sigma,applicand) =
@@ -485,7 +485,7 @@ 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 sigma goal goalacc (EConstr.of_constr c1) harg in
       (acc, subst1 harg b, sigma), arg
     | _ ->
       let env = Goal.V82.env sigma goal in
@@ -577,7 +577,6 @@ let convert_hyp ~check ~reorder env sigma d =
 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
   check_meta_variables env sigma r;
   let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl r in
   let sgl = List.rev sgl in
diff --git a/proofs/logic.mli b/proofs/logic.mli
index ef8b2731b2..5d21474394 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -33,7 +33,7 @@ val prim_refiner : check:bool -> constr -> evar_map -> Goal.goal -> Goal.goal li
 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
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 41f2ab9c63..4fe3f07d6e 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 () ++
-- 
cgit v1.2.3


From 65551cdf811a1bf428fcdc7e3e5c51df0fffcb78 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 12 May 2020 12:13:50 +0200
Subject: Wrap the legacy refiner type into the Logic API.

---
 proofs/clenvtac.ml |  1 -
 proofs/logic.ml    | 13 +++++++++++--
 proofs/logic.mli   |  2 +-
 proofs/refiner.ml  | 14 +-------------
 4 files changed, 13 insertions(+), 17 deletions(-)

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 4eb8658f83..b12d966387 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -581,10 +581,19 @@ let prim_refiner r sigma goal =
   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)
+  { Evd.it = sgl; Evd.sigma = sigma; }
 
-let prim_refiner ~check r sigma goal =
+let refiner ~check r { Evd.sigma = sigma; Evd.it = goal } =
   if check then
     with_check (prim_refiner r sigma) goal
   else
     prim_refiner r sigma goal
+
+(* 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)
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 5d21474394..e4fed22860 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -26,7 +26,7 @@ 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. } *)
 
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       *)
-- 
cgit v1.2.3


From 8bc79fd74ff347d93758ca5c088b085f721819fb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 12 May 2020 12:58:35 +0200
Subject: Remove useless try-with clauses in newring.

This is already protected by then enter block.
---
 plugins/setoid_ring/newring.ml | 32 ++++++++++++++------------------
 1 file changed, 14 insertions(+), 18 deletions(-)

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
-- 
cgit v1.2.3


From 5530ac6ee1fd533a2b56944bd9e16b0d767f3e61 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 12 May 2020 13:57:50 +0200
Subject: Remove legacy Refiner error constructors.

They were not used anywhere anymore.
---
 proofs/logic.ml  | 2 --
 proofs/logic.mli | 2 --
 vernac/himsg.ml  | 9 ---------
 3 files changed, 13 deletions(-)

diff --git a/proofs/logic.ml b/proofs/logic.ml
index b12d966387..eb0ce23ab7 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -31,13 +31,11 @@ type refiner_error =
   | 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
diff --git a/proofs/logic.mli b/proofs/logic.mli
index e4fed22860..9dc75000a1 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -36,13 +36,11 @@ type refiner_error =
   | 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/vernac/himsg.ml b/vernac/himsg.ml
index 4fe3f07d6e..9d67ce3757 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -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
-- 
cgit v1.2.3


From b3b967385830daa09a149e093fa6352a99884436 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 12 May 2020 14:07:16 +0200
Subject: Clean up the legacy refiner implementation.

We avoid using global-access primitives and instead rely on purely functional
passing of the relevant data. Namely, we replace the goal argument with its
environment, and we pass the additional check parameter.
---
 proofs/logic.ml | 112 ++++++++++++++++++++++++++------------------------------
 1 file changed, 51 insertions(+), 61 deletions(-)

diff --git a/proofs/logic.ml b/proofs/logic.ml
index eb0ce23ab7..812fd1d769 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -71,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
 
 (************************************************************************)
 (************************************************************************)
@@ -314,8 +312,8 @@ 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 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
@@ -332,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 conclty in
-          if !check && occur_meta sigma conclty then
+          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
@@ -361,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 (EConstr.of_constr 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
@@ -386,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
@@ -414,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 (EConstr.of_constr 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) =
@@ -443,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
@@ -460,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)
@@ -483,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 (EConstr.of_constr 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
@@ -503,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
@@ -537,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
 
@@ -572,20 +565,17 @@ let convert_hyp ~check ~reorder env sigma d =
 (************************************************************************)
 (* Primitive tactics are handled here *)
 
-let prim_refiner r sigma goal =
+let prim_refiner ~check r sigma goal =
   let env = Goal.V82.env sigma goal in
   let cl = Goal.V82.concl sigma goal in
   check_meta_variables env sigma r;
-  let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl r in
+  let (sgl,cl',sigma,oterm) = mk_refgoals ~check env sigma [] cl r in
   let sgl = List.rev sgl in
   let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in
   { Evd.it = sgl; Evd.sigma = sigma; }
 
 let refiner ~check r { Evd.sigma = sigma; Evd.it = goal } =
-  if check then
-    with_check (prim_refiner r sigma) goal
-  else
-    prim_refiner r sigma goal
+  prim_refiner ~check r sigma goal
 
 (* Profiling refiner *)
 let refiner ~check =
-- 
cgit v1.2.3


From 20ed9460ec30d7b02aa074c234014f0f2d86ecd3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 12 May 2020 15:06:28 +0200
Subject: Write the outermost part of the legacy refiner directly in the monad.

---
 proofs/logic.ml | 31 +++++++++++++------------------
 1 file changed, 13 insertions(+), 18 deletions(-)

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 812fd1d769..c7a1c32e7c 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -565,23 +565,18 @@ let convert_hyp ~check ~reorder env sigma d =
 (************************************************************************)
 (* Primitive tactics are handled here *)
 
-let prim_refiner ~check r sigma goal =
-  let env = Goal.V82.env sigma goal in
-  let cl = Goal.V82.concl sigma goal 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 ~check env sigma [] cl r in
-  let sgl = List.rev sgl in
-  let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in
-  { Evd.it = sgl; Evd.sigma = sigma; }
-
-let refiner ~check r { Evd.sigma = sigma; Evd.it = goal } =
-  prim_refiner ~check r sigma goal
-
-(* 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 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
-- 
cgit v1.2.3


From c5fdfe6ffef15795ecfde8f18f332ddefd35605e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 12 May 2020 15:50:02 +0200
Subject: Remove a unused legacy tactic from Clenv.

---
 proofs/clenv.ml  | 4 ----
 proofs/clenv.mli | 3 ---
 2 files changed, 7 deletions(-)

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
 
-- 
cgit v1.2.3