diff options
| author | herbelin | 2010-10-31 21:19:29 +0000 |
|---|---|---|
| committer | herbelin | 2010-10-31 21:19:29 +0000 |
| commit | 841bc4617470a30d4025fc279c5a3e72edbb6e13 (patch) | |
| tree | 07d18ac3c7a4ae7908b3545590248c841232b348 /plugins | |
| parent | 30f6fd59780f57201e93ef4986422b6c89077ab4 (diff) | |
An experimental support for open constrs in hints and in "using"
option of "auto". Works for not too complicated hints (e.g. "@pair _ _ 0").
Would be simpler if make_apply_entry supported lemmas containing evars.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13598 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 43658e8021..e047f13d53 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1450,7 +1450,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = Eauto.eauto_with_bases false (true,5) - [Lazy.force refl_equal] + [Evd.empty,Lazy.force refl_equal] [Auto.Hint_db.empty empty_transparent_state false] ) ) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 057ffb9b32..f066e39d05 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1005,7 +1005,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ Eauto.eauto_with_bases false (true,5) - [delayed_force refl_equal] + [Evd.empty,delayed_force refl_equal] [Auto.Hint_db.empty empty_transparent_state false] ] ) |