aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/wg_Find.ml
Commit message (Expand)AuthorAge
* Removed a unused and troublesome feature in CoqIDE that handled shortcuts the...Gravatar ppedrot2012-04-24
* Fixed bad gravity of mark that would make CoqIDE loop whenever Replace All wa...Gravatar ppedrot2012-04-23
* Cleaning a bit previous commitGravatar ppedrot2012-04-23
* Now CoqIDE has a nice find & replace mechanism. BTW, removing a blob of dead ...Gravatar ppedrot2012-04-23