12345678910111213141516171819202122232425262728293031323334(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)type'at={v:'a;loc:Loc.toption;}letmake?locv={v;loc}letmapfn={nwithv=fn.v}letmap_with_locfn={nwithv=f?loc:n.locn.v}letmap_from_locfl=letloc,v=lin{v=f?locv;loc}letwith_valfn=fn.vletwith_loc_valfn=f?loc:n.locn.vleteqfxy=fx.vy.vmoduleSmart=structletmapfn=letv'=fn.vinifv'==n.vthennelse{nwithv=v'}end