diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-15 14:03:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-15 14:07:13 +0200 |
| commit | aae3c3b42a9bad20ebde4a139e6de660fbb8e042 (patch) | |
| tree | 188895bdaa3835f6175406fb0d22e282441448a5 /proofs/refiner.ml | |
| parent | c69404402212ed9d541899ae78ac889e62cf238a (diff) | |
Removing unused Refiner.tclWITHHOLES.
Diffstat (limited to 'proofs/refiner.ml')
| -rw-r--r-- | proofs/refiner.ml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 6e398b61e..ba319fdc0 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -369,11 +369,3 @@ let check_evars env sigma extsigma origsigma = let gl_check_evars env sigma extsigma gl = let origsigma = gl.sigma in check_evars env sigma extsigma origsigma - -let tclWITHHOLES accept_unresolved_holes tac sigma c gl = - if sigma == project gl then tac c gl - else - let res = tclTHEN (tclEVARS sigma) (tac c) gl in - if not accept_unresolved_holes then - gl_check_evars (pf_env gl) (res).sigma sigma gl; - res |