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/logic.ml | |
| parent | 0f7462cc5f8676edaa6b7052edaad40e32fc8234 (diff) | |
Avoid passing dummy env to error printer
Diffstat (limited to 'proofs/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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) |