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 | |
| 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')
| -rw-r--r-- | doc/plugin_tutorial/tuto3/src/construction_game.ml | 5 | ||||
| -rw-r--r-- | doc/plugin_tutorial/tuto3/src/tuto_tactic.ml | 10 |
2 files changed, 8 insertions, 7 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 () = diff --git a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml index 8f2c387d09..2d541087ce 100644 --- a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml +++ b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml @@ -116,11 +116,11 @@ let repackage i h_hyps_id = Goal.enter begin fun gl -> mkApp (c_U (), [| ty2; mkVar h_hyps_id|]) |]) in Refine.refine ~typecheck:true begin fun evd -> let evd, new_goal = Evarutil.new_evar env evd - (mkProd (Names.Name.Anonymous, - mkApp(c_H (), [| new_packed_type |]), - Vars.lift 1 concl)) in - evd, mkApp (new_goal, - [|mkApp(c_M (), [|new_packed_type; new_packed_value |]) |]) + (mkArrowR (mkApp(c_H (), [| new_packed_type |])) + (Vars.lift 1 concl)) + in + evd, mkApp (new_goal, + [|mkApp(c_M (), [|new_packed_type; new_packed_value |]) |]) end end |