diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-11-27 09:28:09 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-11-28 19:21:24 +0100 |
| commit | 34815f0c8fae4c87798b18f7343c1f1afc3056eb (patch) | |
| tree | daaa3b44d5ae0016a6cbfb78f9582b170c080568 | |
| parent | 5d3f5c210aad8d73b007936e65694c401e66c7d0 (diff) | |
Tactic primitives: missing [advance] lead to spurious dangling goals.
Closes #3801.
| -rw-r--r-- | proofs/proofview.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index c85021138..15110a67c 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -408,7 +408,8 @@ let iter_goal i = i goal >> Proof.map (fun comb -> comb :: subgoals) Comb.get end [] initial >>= fun subgoals -> - Comb.set (CList.flatten (CList.rev subgoals)) + Solution.get >>= fun evd -> + Comb.set CList.(undefined evd (flatten (rev subgoals))) (** A variant of [Monad.List.fold_left2] where the first list is the list of focused goals. The argument tactic is executed in a focus @@ -431,7 +432,8 @@ let fold_left2_goal i s l = i goal a r >>= fun r -> Proof.map (fun comb -> (r, comb :: subgoals)) Comb.get end (s,[]) initial.comb l >>= fun (r,subgoals) -> - Comb.set (CList.flatten (CList.rev subgoals)) >> + Solution.get >>= fun evd -> + Comb.set CList.(undefined evd (flatten (rev subgoals))) >> return r (** Dispatch tacticals are used to apply a different tactic to each @@ -1060,6 +1062,7 @@ module V82 = struct in let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in let sgs = CList.flatten goalss in + let sgs = undefined evd sgs in InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >> Pv.set { solution = evd; comb = sgs; } with e when catchable_exception e -> |