diff options
Diffstat (limited to 'contrib/funind')
| -rw-r--r-- | contrib/funind/functional_principles_proofs.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index 3d80bd0040..d7bcde69cb 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -1399,7 +1399,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = false (true,5) [Lazy.force refl_equal] - [empty_transparent_state, Auto.Hint_db.empty] + [Auto.Hint_db.empty false] ) ) ) |