math-comp / trajectories

0 stars 4 forks source link

ler_absr_eval_pol #6

Closed affeldt-aist closed 1 year ago

affeldt-aist commented 2 years ago

https://github.com/affeldt-aist/trajectories/blob/b8fd342ec8c7f5e7a3d07a2172aa710ba2694797/theories/ssr_descartes/civt.v#L46

Where is it defined? @ybertot

affeldt-aist commented 1 year ago

we could actually find it in cmvt.v in an older commit