diff options
| author | Pierre-Marie Pédrot | 2019-03-15 14:19:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-03-15 14:19:51 +0100 |
| commit | ed275fd5eb8b11003f8904010d853d2bd568db79 (patch) | |
| tree | e27b7778175cb0d9d19bd8bde9c593b335a85125 /doc/plugin_tutorial/tuto3 | |
| parent | a44c4a34202fa6834520fcd6842cc98eecf044ec (diff) | |
| parent | 1ba29c062e30181bda9d931dffe48e457dfee9d6 (diff) | |
Merge PR #8817: SProp: the definitionally proof irrelevant universe
Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82
Diffstat (limited to 'doc/plugin_tutorial/tuto3')
| -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 |