From 01a673e8d8e22e7aaebe5dc4e801d36ce29941b7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 9 Nov 2018 15:58:52 +0100
Subject: Adapt to coq/coq#8933 (Make initial evar map argument to
 check_evars_are_solved optional)

---
 tuto3/src/construction_game.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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)
 
-- 
cgit v1.2.3