diff options
| author | Maxime Dénès | 2018-10-30 12:48:16 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-30 13:11:30 +0100 |
| commit | 1b35eebd0ac45233ec1714a4040eddedf0d656f5 (patch) | |
| tree | 6e3aef35bdada8ab2dd06df2b48a35bb4e059748 /proofs | |
| parent | 0f7462cc5f8676edaa6b7052edaad40e32fc8234 (diff) | |
Avoid passing dummy env to error printer
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/goal.ml | 8 | ||||
| -rw-r--r-- | proofs/goal.mli | 4 | ||||
| -rw-r--r-- | proofs/logic.ml | 2 |
3 files changed, 7 insertions, 7 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 4e540de538..7245d4a004 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -72,18 +72,18 @@ module V82 = struct (evk, ev, evars) (* Instantiates a goal with an open term *) - let partial_solution sigma evk c = + let partial_solution env sigma evk c = (* Check that the goal itself does not appear in the refined term *) let _ = if not (Evarutil.occur_evar_upto sigma evk c) then () - else Pretype_errors.error_occur_check Environ.empty_env sigma evk c + else Pretype_errors.error_occur_check env sigma evk c in Evd.define evk c sigma (* Instantiates a goal with an open term, using name of goal for evk' *) - let partial_solution_to sigma evk evk' c = + let partial_solution_to env sigma evk evk' c = let id = Evd.evar_ident evk sigma in - let sigma = partial_solution sigma evk c in + let sigma = partial_solution env sigma evk c in match id with | None -> sigma | Some id -> Evd.rename evk' id sigma diff --git a/proofs/goal.mli b/proofs/goal.mli index 3b31cff8d7..af9fb662bf 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -48,11 +48,11 @@ module V82 : sig goal * EConstr.constr * Evd.evar_map (* Instantiates a goal with an open term *) - val partial_solution : Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map + val partial_solution : Environ.env -> Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map (* Instantiates a goal with an open term, reusing name of goal for second goal *) - val partial_solution_to : Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map + val partial_solution_to : Environ.env -> Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map (* Principal part of the progress tactical *) val progress : goal list Evd.sigma -> goal Evd.sigma -> bool diff --git a/proofs/logic.ml b/proofs/logic.ml index 254c93d0a2..b8612cd2c0 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -590,5 +590,5 @@ let prim_refiner r sigma goal = check_meta_variables env sigma c; let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in let sgl = List.rev sgl in - let sigma = Goal.V82.partial_solution sigma goal (EConstr.of_constr oterm) in + let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in (sgl, sigma) |