Skip to content

String_ident tweaks

Robbert Krebbers requested to merge robbert/string_ident_tweaks into master
  • Add types to Ltac2 for string_ident.
  • Avoid duplicating Ltac2 Option.get.

Merge request reports