diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-12 16:58:37 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-12 16:59:53 +0200 |
| commit | e4aa9817115b3d27eb7fca8fed86ffe397b868ad (patch) | |
| tree | efa8a3250bffa0a6fd7ac7d8c0f07ee17bc53734 /proofs/proofview.ml | |
| parent | 5dc8187aa8e6b481338035a022fec4025a25eb33 (diff) | |
While we don't have a clean alternative to Clenvtac, add a primitive
for tclEVARS which might solve existing goals.
Diffstat (limited to 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index bc6ce4fc6..a97add1ce 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -804,6 +804,9 @@ module V82 = struct let tclEVARS evd = Proof.modify (fun ps -> { ps with solution = evd }) + let tclEVARSADVANCE evd = + Proof.modify (fun ps -> { solution = evd; comb = undefined evd ps.comb }) + let tclEVARUNIVCONTEXT ctx = Proof.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx }) |