Clenvtac.clenv_refine in the new monad. Not satisfactory though, because it

exhibits the "useless goal" behaviour: there is code out there depending on
the fact that goals cannot be solved by side effects.

6 files changed, 17 insertions, 12 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index e8af6ffbd..b2fea6fd1 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -59,7 +59,11 @@ let clenv_pose_dependent_evars with_evars clenv =
       (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
   clenv_pose_metas_as_evars clenv dep_mvs
 
-let clenv_refine with_evars ?(with_classes=true) clenv gls =
+let clenv_refine with_evars ?(with_classes=true) clenv =
+  (** ppedrot: a Goal.enter here breaks things, because the tactic below may
+      solve goals by side effects, while the compatibility layer keeps those
+      useless goals. That deserves a FIXME. *)
+  Proofview.V82.tactic begin fun gl ->
   let clenv = clenv_pose_dependent_evars with_evars clenv in
   let evd' =
     if with_classes then
@@ -71,16 +75,17 @@ let clenv_refine with_evars ?(with_classes=true) clenv gls =
   let clenv = { clenv with evd = evd' } in
   tclTHEN
     (tclEVARS (Evd.clear_metas evd'))
-    (refine_no_check (clenv_cast_meta clenv (clenv_value clenv)))
-    gls
+    (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl
+  end
 
 open Unification
 
 let dft = default_unify_flags
 
 let res_pf clenv ?(with_evars=false) ?(flags=dft ()) =
-  Proofview.V82.tactic begin fun gl ->
-    clenv_refine with_evars (clenv_unique_resolver ~flags clenv gl) gl
+  Proofview.Goal.raw_enter begin fun gl ->
+    let clenv gl = clenv_unique_resolver ~flags clenv gl in
+    clenv_refine with_evars (Tacmach.New.of_old clenv (Proofview.Goal.assume gl))
   end
 
 (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index eea32019e..789a21c24 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -14,7 +14,7 @@ open Unification
 
 (** Tactics *)
 val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic
-val clenv_refine : evars_flag -> ?with_classes:bool -> clausenv -> tactic
+val clenv_refine : evars_flag -> ?with_classes:bool -> clausenv -> unit Proofview.tactic
 val res_pf : clausenv -> ?with_evars:evars_flag -> ?flags:unify_flags -> unit Proofview.tactic
 
 val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 80aa9b660..e7082a579 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1136,13 +1136,13 @@ let unify_resolve_nodelta poly (c,clenv) gl =
   let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
   let clenv' = connect_clenv gl clenv' in
   let clenv'' = clenv_unique_resolver ~flags:auto_unif_flags clenv' gl in
-  Clenvtac.clenv_refine false clenv'' gl
+  Proofview.V82.of_tactic (Clenvtac.clenv_refine false clenv'') gl
 
 let unify_resolve poly flags (c,clenv) gl =
   let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
   let clenv' = connect_clenv gl clenv' in
   let clenv'' = clenv_unique_resolver ~flags clenv' gl in
-  Clenvtac.clenv_refine false clenv'' gl
+  Proofview.V82.of_tactic (Clenvtac.clenv_refine false clenv'') gl
 
 let unify_resolve_gen poly = function
   | None -> unify_resolve_nodelta poly
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index f11c027ad..7c9aa59b6 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -104,13 +104,13 @@ let unify_e_resolve poly flags (c,clenv) gls =
   let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
   let clenv' = connect_clenv gls clenv' in
   let clenv' = clenv_unique_resolver ~flags clenv' gls in
-    Clenvtac.clenv_refine true ~with_classes:false clenv' gls
+  Proofview.V82.of_tactic (Clenvtac.clenv_refine true ~with_classes:false clenv') gls
 
 let unify_resolve poly flags (c,clenv) gls =
   let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
   let clenv' = connect_clenv gls clenv' in
   let clenv' = clenv_unique_resolver ~flags clenv' gls in
-    Clenvtac.clenv_refine false(*uhoh, was true*) ~with_classes:false clenv' gls
+  Proofview.V82.of_tactic (Clenvtac.clenv_refine false(*uhoh, was true*) ~with_classes:false clenv') gls
 
 let clenv_of_prods poly nprods (c, clenv) gls =
   if poly || Int.equal nprods 0 then Some clenv
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 4d6893f1c..fcce6e5eb 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -592,7 +592,7 @@ module New = struct
     in
     let branchtacs = List.init (Array.length branchsigns) after_tac in
     Proofview.tclTHEN
-      (Proofview.V82.tactic (Clenvtac.clenv_refine false clenv'))
+      (Clenvtac.clenv_refine false clenv')
       (Proofview.tclEXTEND [] tclIDTAC branchtacs)
     end
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5931257d2..3c0016830 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3229,7 +3229,7 @@ let induction_tac_felim with_evars indvars nparams elim gl =
   let elimclause' = recolle_clenv nparams indvars elimclause gl in
   (* one last resolution (useless?) *)
   let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in
-  Clenvtac.clenv_refine with_evars resolved gl
+  Proofview.V82.of_tactic (Clenvtac.clenv_refine with_evars resolved) gl
 
 (* Apply induction "in place" replacing the hypothesis on which
    induction applies with the induction hypotheses *)