Making Proofview independent of Logic.

5 files changed, 14 insertions, 10 deletions

diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 2b9db60b4..6f52b3ee9 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -154,8 +154,8 @@ end
     focused goals. *)
 type proofview = {
   solution : Evd.evar_map;
-  comb : Goal.goal list;
-  shelf : Goal.goal list;
+  comb : Evar.t list;
+  shelf : Evar.t list;
 }
 
 (** {6 Instantiation of the logic monad} *)
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index 7a6ea10fe..0aff0a720 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -70,8 +70,8 @@ end
     focused goals. *)
 type proofview = {
   solution : Evd.evar_map;
-  comb : Goal.goal list;
-  shelf : Goal.goal list;
+  comb : Evar.t list;
+  shelf : Evar.t list;
 }
 
 (** {6 Instantiation of the logic monad} *)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 2a09d52f7..f42a60d9d 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -625,18 +625,18 @@ let shelve_unifiable =
   InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_unifiable")) >>
   Shelf.modify (fun gls -> gls @ u)
 
-(** [guard_no_unifiable] fails with error [UnresolvedBindings] if some
+(** [guard_no_unifiable] returns the list of unifiable goals if some
     goals are unifiable (see {!shelve_unifiable}) in the current focus. *)
 let guard_no_unifiable =
   let open Proof in
   Pv.get >>= fun initial ->
   let (u,n) = partition_unifiable initial.solution initial.comb in
   match u with
-  | [] -> tclUNIT ()
+  | [] -> tclUNIT None
   | gls ->
       let l = CList.map (fun g -> Evd.dependent_evar_ident g initial.solution) gls in
       let l = CList.map (fun id -> Names.Name id) l in
-      tclZERO (Logic.RefinerError (Logic.UnresolvedBindings l))
+      tclUNIT (Some l)
 
 (** [unshelve l p] adds all the goals in [l] at the end of the focused
     goals of p *)
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 61014468b..20f67f258 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -295,9 +295,9 @@ val shelve : unit tactic
     considered). *)
 val shelve_unifiable : unit tactic
 
-(** [guard_no_unifiable] fails with error [UnresolvedBindings] if some
+(** [guard_no_unifiable] returns the list of unifiable goals if some
     goals are unifiable (see {!shelve_unifiable}) in the current focus. *)
-val guard_no_unifiable : unit tactic
+val guard_no_unifiable : Names.Name.t list option tactic
 
 (** [unshelve l p] adds all the goals in [l] at the end of the focused
     goals of p *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f725a0654..ffe10d81c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -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 ->
@@ -4129,7 +4133,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
           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 ();