diff options
| -rw-r--r-- | tuto3/src/tuto_tactic.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tuto3/src/tuto_tactic.ml b/tuto3/src/tuto_tactic.ml index 708b9c1877..cb73a4486b 100644 --- a/tuto3/src/tuto_tactic.ml +++ b/tuto3/src/tuto_tactic.ml @@ -104,7 +104,6 @@ let get_type_of_hyp env id = let repackage i h_hyps_id = Goal.enter begin fun gl -> let env = Goal.env gl in - let store = Goal.extra gl in let evd = Tacmach.New.project gl in let concl = Tacmach.New.pf_concl gl in let (ty1 : EConstr.t) = get_type_of_hyp env i in @@ -116,7 +115,7 @@ let repackage i h_hyps_id = Goal.enter begin fun gl -> mkApp (c_R (), [| ty1; ty2; mkVar i; 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 ~store + let evd, new_goal = Evarutil.new_evar env evd (mkProd (Names.Name.Anonymous, mkApp(c_H (), [| new_packed_type |]), Vars.lift 1 concl)) in |