Re-implement passing identifier back to Ltac1
This implementation avoids use of Unsafe, so it is compatible with v8.11 and forward, and also has the benefit of being simpler.
Merge request reports
Activity
Please register or sign in to reply
This implementation avoids use of Unsafe, so it is compatible with v8.11 and forward, and also has the benefit of being simpler.