Skip to content

Latest commit

 

History

History
6 lines (6 loc) · 277 Bytes

17704-open-constr-no-expand.rst

File metadata and controls

6 lines (6 loc) · 277 Bytes
  • Changed: open_constr in Ltac1 and Ltac2 does not perform evar normalization. Normalization may be recovered using let c := open_constr:(...) in constr:(c) if necessary for performance (#17704, by Gaëtan Gilbert).