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

7 files changed, 29 insertions, 1 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 028361185..f85970a1f 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1572,6 +1572,12 @@ let evar_source_of_meta mv evd =
   | Anonymous -> (Loc.ghost,Evar_kinds.GoalEvar)
   | Name id -> (Loc.ghost,Evar_kinds.VarInstance id)
 
+let dependent_evar_ident ev evd =
+  let evi = find evd ev in
+  match evi.evar_source with
+  | (_,Evar_kinds.VarInstance id) -> id
+  | _ -> anomaly (str "Not an evar resulting of a dependent binding")
+
 (*******************************************************************)
 type open_constr = evar_map * constr
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 467e1a163..542e2342f 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -264,6 +264,9 @@ val rename : existential_key -> Id.t -> evar_map -> evar_map
 val evar_key : Id.t -> evar_map -> existential_key
 
 val evar_source_of_meta : metavariable -> evar_map -> Evar_kinds.t located
+
+val dependent_evar_ident : existential_key -> evar_map -> Id.t
+
 (** {5 Side-effects} *)
 
 val emit_side_effects : Declareops.side_effects -> evar_map -> evar_map
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 631c2428e..4a1b6bfc0 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 d31a51fbd..d04861c12 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 ab5cf52d4..bfb36824d 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 04c084fb7..e19236df0 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 e2d331c67..671bd414e 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