diff options
Diffstat (limited to 'doc/plugin_tutorial/tuto3/src/tuto_tactic.ml')
| -rw-r--r-- | doc/plugin_tutorial/tuto3/src/tuto_tactic.ml | 10 |
1 files changed, 5 insertions, 5 deletions
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 |