Adding a tactic which fails if one of the goals under focus is dependent in another one.

5 files changed, 20 insertions, 1 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 631c2428ec..4a1b6bfc05 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -35,6 +35,8 @@ let pr_goal {content = e} = str "GOAL:" ++ Pp.int (Evar.repr e)
 
 let goal_ident sigma {content = e} = Evd.evar_ident e sigma
 
+let dependent_goal_ident sigma {content = e} = Evd.dependent_evar_ident e sigma
+
 (* access primitive *)
 (* invariant : [e] must exist in [em] *)
 let content evars { content = e } = Evd.find evars e
diff --git a/proofs/goal.mli b/proofs/goal.mli
index d31a51fbd4..d04861c122 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -27,6 +27,8 @@ val pr_goal : goal -> Pp.std_ppcmds
 
 val goal_ident : Evd.evar_map -> goal -> Names.Id.t
 
+val dependent_goal_ident : Evd.evar_map -> goal -> Names.Id.t
+
 (* [advance sigma g] returns [Some g'] if [g'] is undefined and 
     is the current avatar of [g] (for instance [g] was changed by [clear]
     into [g']). It returns [None] if [g] has been (partially) solved. *)
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index ab5cf52d46..bfb36824d3 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -6,11 +6,11 @@ Proof_type
 Proof_errors
 Proofview_gen
 Proofview_monad
+Logic
 Proofview
 Proof
 Proof_global
 Redexpr
-Logic
 Refiner
 Tacmach
 Pfedit
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 04c084fb77..e19236df04 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -663,6 +663,17 @@ let shelve_unifiable =
   Proof.set {initial with comb=n} >>
   Proof.put (true,(u,[]))
 
+let check_no_dependencies =
+  let (>>=) = Proof.bind in
+  Proof.get >>= fun initial ->
+  let (u,n) = Goal.partition_unifiable initial.solution initial.comb in
+  match u with
+  | [] -> tclUNIT ()
+  | gls ->
+      let l = List.map (Goal.dependent_goal_ident initial.solution) gls in
+      let l = List.map (fun id -> Names.Name id) l in
+      tclZERO (Logic.RefinerError (Logic.UnresolvedBindings l))
+
 (* [unshelve l p] adds all the goals in [l] at the end of the focused
    goals of p *)
 let unshelve l p =
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index e2d331c67c..671bd414ea 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -267,6 +267,10 @@ val shelve : unit tactic
    considered). *)
 val shelve_unifiable : unit tactic
 
+(* This fails with error UnresolvedBindings if some goals are
+   dependent in the current list of goals under focus *)
+val check_no_dependencies : unit tactic
+
 (* [unshelve l p] adds all the goals in [l] at the end of the focused
    goals of p *)
 val unshelve : Goal.goal list -> proofview -> proofview