Hello,

I want to use tactic `make_tp`

inside proof. But receive error (*The reference Transparent was not found in the current environment*)

```
Definition number_10001 : Z.t := 10001.
Opaque number_10001.
Definition number_10000 : Z.t := 10000.
Opaque number_10000.
Ltac make_tp := Transparent number_10000; Transparent number_10001.
```

How can I do that? My problem is that I have several such `number`

definitions and I need to switch between them inside proof (make transparent / make opaque).

https://coq.github.io/doc/master/refman/proofs/writing-proofs/equality.html#coq:tacn.with_strategy

Thank you!

Last updated: Jun 24 2024 at 00:02 UTC