diff options
| author | Gaëtan Gilbert | 2017-10-31 17:04:02 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 13:27:38 +0100 |
| commit | 23f84f37c674a07e925925b7e0d50d7ee8414093 (patch) | |
| tree | 7e470de5769c994d8df37c44fed12cf299d5b194 /doc/plugin_tutorial/tuto3/src/construction_game.ml | |
| parent | 75508769762372043387c67a9abe94e8f940e80a (diff) | |
Add relevance marks on binders.
Kernel should be mostly correct, higher levels do random stuff at
times.
Diffstat (limited to 'doc/plugin_tutorial/tuto3/src/construction_game.ml')
| -rw-r--r-- | doc/plugin_tutorial/tuto3/src/construction_game.ml | 5 |
1 files changed, 3 insertions, 2 deletions
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 () = |