From 23f84f37c674a07e925925b7e0d50d7ee8414093 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 31 Oct 2017 17:04:02 +0100
Subject: Add relevance marks on binders.

Kernel should be mostly correct, higher levels do random stuff at
times.
---
 doc/plugin_tutorial/tuto3/src/construction_game.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'doc/plugin_tutorial/tuto3/src/construction_game.ml')

diff --git a/doc/plugin_tutorial/tuto3/src/construction_game.ml b/doc/plugin_tutorial/tuto3/src/construction_game.ml
index 9d9f894e18..663113d012 100644
--- a/doc/plugin_tutorial/tuto3/src/construction_game.ml
+++ b/doc/plugin_tutorial/tuto3/src/construction_game.ml
@@ -1,4 +1,5 @@
 open Pp
+open Context
 
 let find_reference = Coqlib.find_reference [@ocaml.warning "-3"]
 
@@ -32,7 +33,7 @@ let dangling_identity env evd =
   let evd, arg_type = Evarutil.new_evar env evd type_type in
 (* Notice the use of a De Bruijn index for the inner occurrence of the
   bound variable. *)
-  evd, EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type,
+  evd, EConstr.mkLambda(nameR (Names.Id.of_string "x"), arg_type,
           EConstr.mkRel 1)
 
 let dangling_identity2 env evd =
@@ -40,7 +41,7 @@ let dangling_identity2 env evd =
   is meant to be a type. *)
   let evd, (arg_type, type_type) =
     Evarutil.new_type_evar env evd Evd.univ_rigid in
-  evd, EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type,
+  evd, EConstr.mkLambda(nameR (Names.Id.of_string "x"), arg_type,
           EConstr.mkRel 1)
 
 let example_sort_app_lambda () =
-- 
cgit v1.2.3