diff options
| author | Matthieu Sozeau | 2018-10-12 14:43:43 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-10-26 18:30:01 +0200 |
| commit | e3157aa44ba2ebec266e16ae0da78d735d21e779 (patch) | |
| tree | 9aa768084c8098a16a25e53dbfcef62852078f41 | |
| parent | 94ac6fe784c31968b9fd1f2a69464dc22043ed82 (diff) | |
PR 8671: Remove store / goal extra argument
| -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 |