aboutsummaryrefslogtreecommitdiff
path: root/pretyping/ltac_pretype.ml
AgeCommit message (Collapse)Author
2018-09-10Temptative clarification of the role of ltac_genargs field in ltac_var_map.Hugo Herbelin
2017-10-25[general] Remove Econstr dependency from `intf`Emilio Jesus Gallego Arias
To this extent we factor out the relevant bits to a new file, ltac_pretype.