diff options
| author | Gaëtan Gilbert | 2018-11-09 15:58:52 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-09 15:58:52 +0100 |
| commit | 01a673e8d8e22e7aaebe5dc4e801d36ce29941b7 (patch) | |
| tree | 7cf4f22d68df02511396fe32b09c860863285359 | |
| parent | e6f4d7f40b4764b3ef7c9e996003b5e614d3ae2e (diff) | |
Adapt to coq/coq#8933 (Make initial evar map argument to check_evars_are_solved optional)
| -rw-r--r-- | tuto3/src/construction_game.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tuto3/src/construction_game.ml b/tuto3/src/construction_game.ml index 831349c8cc..22b02f6893 100644 --- a/tuto3/src/construction_game.ml +++ b/tuto3/src/construction_game.ml @@ -136,7 +136,7 @@ let example_classes n = (* Question to coq developers: why do we pass two evd arguments to solve_remaining_evars? Is the choice of evd0 relevant here? *) let evd = Pretyping.solve_remaining_evars - (Pretyping.default_inference_flags true) env evd evd0 in + (Pretyping.default_inference_flags true) env evd ~initial:evd0 in let evd, final_type = Typing.type_of env evd proved_equality in Feedback.msg_notice (Printer.pr_econstr_env env evd proved_equality) |