diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index f0e9842fa3..b78291ecde 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -191,12 +191,9 @@ let make_exact_entry (c,cty) = (head_of_constr_reference (List.hd (head_constr cty)), { pri=0; pat=None; code=Give_exact c }) -let dummy_goal = - {it={evar_hyps=empty_named_context_val; - evar_concl=mkProp; - evar_body=Evar_empty; - evar_extra=None}; - sigma=Evd.empty} +let dummy_goal = + {it = make_evar empty_named_context_val mkProp; + sigma = empty} let make_apply_entry env sigma (eapply,verbose) (c,cty) = let cty = hnf_constr env sigma cty in |