proof-general/contrib, branch master Emacs plugins for proof management systems Remove mmm and ML4PG contribs and remove references to them in code and docs 2017-05-24T15:14:51+00:00 Paul Steckler 2017-05-24T15:14:51+00:00 c9e9c691c353d5d4835551de8d7d1f4c0ec74b9f 






Add file contrib/mmm/.nosearch to help feature extraction tools
2017-04-18T18:17:09+00:00

Jonas Bernoulli

2017-04-18T16:18:31+00:00

28ee469c90b9673cce21c1ea4e34d5dc3406ad56

This change is intended as an intermediate step toward the removal
of the bundled copy of `mmm' package.  Even with this change, PG
continues to use the bundled version, unless `mmm-auto' is already
loaded at the time PG first loads `proof-auxmodes'.

The benefit of this change is that tools that extract the features
provided and required by a package, such as those used to maintain
the Emacsmirror, will no longer be tricked into believing that
`mmm' is part of PG.

Eventually the bundled `mmm' copy should be removed completely, as I
suggested in #171, and as was already on the roadmap before I did so.





This change is intended as an intermediate step toward the removal
of the bundled copy of `mmm' package.  Even with this change, PG
continues to use the bundled version, unless `mmm-auto' is already
loaded at the time PG first loads `proof-auxmodes'.

The benefit of this change is that tools that extract the features
provided and required by a package, such as those used to maintain
the Emacsmirror, will no longer be tricked into believing that
`mmm' is part of PG.

Eventually the bundled `mmm' copy should be removed completely, as I
suggested in #171, and as was already on the roadmap before I did so.







remove backup file
2013-07-11T20:58:36+00:00

Hendrik Tews

2013-07-11T20:58:36+00:00

2902104d6cd9170b43d429c9e593e8bda7329457












Authors of ML4PG
2013-05-31T12:34:49+00:00

joheras

2013-05-31T12:34:49+00:00

5f3115e9412cb3b955e5a79e6867bf949fa64c77












Moving ML4PG from coq directory to contrib directory.
2013-05-31T12:10:57+00:00

joheras

2013-05-31T12:10:57+00:00

daf76667b7212664ce83c8fd5aa5d48cb823e866












Patch: font-lock-beginning-of-syntax-function -> syntax-begin-function to work with Emacs 23.3.  May break work with earlier versions.
2011-04-26T14:34:45+00:00

David Aspinall

2011-04-26T14:34:45+00:00

9429d7e54d4674a43975577927b0e3af0d7f88b5












Renamed file contrib/mmm/version.texi, formerly mmm/version.texi
2010-08-27T11:25:13+00:00

David Aspinall

2010-08-27T11:25:13+00:00

44b88b54d435ac3769c24ccca0462a981eff21ea












Renamed file contrib/mmm/mmm.texinfo, formerly mmm/mmm.texinfo
2010-08-27T11:25:10+00:00

David Aspinall

2010-08-27T11:25:10+00:00

8c55c79574c3078489f98bd8300241b57e9fc33b












Renamed file contrib/mmm/mmm-vars.el, formerly mmm/mmm-vars.el
2010-08-27T11:25:07+00:00

David Aspinall

2010-08-27T11:25:07+00:00

3044f9629320d2d69710a05edf98188977f0f285












Renamed file contrib/mmm/mmm-utils.el, formerly mmm/mmm-utils.el
2010-08-27T11:25:04+00:00

David Aspinall

2010-08-27T11:25:04+00:00

dc1c225560e4e31d215ece2ca11c5e57d1eac567