diff options
Diffstat (limited to 'tactics/autorewrite.ml')
| -rw-r--r-- | tactics/autorewrite.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index a52f24b0ea..c8d1c43703 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -88,9 +88,9 @@ let _ = vinterp_add "HintRewrite" let lcsr = List.map (function | Node(loc,"CONSTR",l) -> - constr_of_Constr (interp_tacarg - (evc,env,[],[],None,Tactic_debug.DebugOff) - (Node(loc,"COMMAND",l))) + let ist = { evc=evc; env=env; lfun=[]; lmatch=[]; + goalopt=None; debug=Tactic_debug.DebugOff } in + constr_of_Constr (interp_tacarg ist (Node(loc,"COMMAND",l))) | _ -> bad_vernac_args "HintRewrite") lcom in add_rew_rules (string_of_id id) (List.map (fun csr -> (csr,ort = "LR",t)) lcsr)) |