diff options
| author | Emilio Jesús Gallego Arias | 2018-11-24 16:35:25 +0100 |
|---|---|---|
| committer | GitHub | 2018-11-24 16:35:25 +0100 |
| commit | b5ebc0a2aa4e73054b6085dd82211a08636c1418 (patch) | |
| tree | cffc64b213d4db3aa42aaa515e894e8b23c21286 | |
| parent | 97f2bae11a12854be3fe442b41c07116a065ee1c (diff) | |
| parent | 01a673e8d8e22e7aaebe5dc4e801d36ce29941b7 (diff) | |
Merge pull request #18 from SkySkimmer/solve-remaining-evars-initial-arg
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) |