diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 18:08:42 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 18:33:06 +0100 |
| commit | b2a2cb77f38549a25417d199e90d745715f3e465 (patch) | |
| tree | 03af99f1fe1233ce4fc8e1defd927b4e845218dc /proofs | |
| parent | 32bf41967bbcd2bf21dea8a6b4f5f500eb15aacc (diff) | |
Making Proofview independent of Logic.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 6 | ||||
| -rw-r--r-- | proofs/proofview.mli | 4 |
2 files changed, 5 insertions, 5 deletions
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 *) |