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/tuto_tactic.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

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

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
 
-- 
cgit v1.2.3