diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5e8869f9b0..5a19f95f90 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -168,7 +168,7 @@ let convert_hyp ?(check=true) d = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let ty = Proofview.Goal.concl gl in - let sign = convert_hyp check (named_context_val env) sigma d in + let sign = convert_hyp ~check env sigma d in let env = reset_with_named_context sign env in Refine.refine ~typecheck:false begin fun sigma -> Evarutil.new_evar env sigma ~principal:true ty @@ -728,7 +728,7 @@ let e_change_in_hyps ?(check=true) f args = raise (RefinerError (env, sigma, NoSuchHyp id)) in let (sigma, d) = e_pf_change_decl redfun where hyp env sigma in - let sign = Logic.convert_hyp check (named_context_val env) sigma d in + let sign = Logic.convert_hyp ~check env sigma d in let env = reset_with_named_context sign env in (env, sigma) in |