Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Removing the Entry module now that rules need not be marshalled. | 2016-05-10 | |
* | Merge branch 'v8.5' | 2016-05-09 | |
|\ | |||
| * | Rename Lexer -> CLexer. | 2016-05-09 | |
* | | Moving the Val module to Geninterp. | 2016-05-04 | |
* | | A note concerning the "Drop" command. | 2016-05-03 | |
* | | setup.txt : a guide explaining taming Emacs, Merlin, Company, Ocamldebug. | 2016-05-03 | |
* | | Merge branch 'v8.5' | 2016-04-09 | |
|\| | |||
* | | Fixing printing of toplevel values. | 2016-04-08 | |
| * | Use -win32 and -win64 suffixes for installer name on Windows. | 2016-04-07 | |
* | | Merge remote-tracking branch 'origin/pr/78' into trunk: | 2016-04-04 | |
|\ \ | |||
* | | | Creating a dedicated ltac/ folder for Hightactics. | 2016-03-21 | |
* | | | Moving Tacenv to Hightactics. | 2016-03-20 | |
* | | | Moving Tactic_debug to Hightactic. | 2016-03-20 | |
* | | | Documenting changes. | 2016-03-20 | |
* | | | Making Evarutil independent from Reductionops. | 2016-03-20 | |
* | | | Splitting Evarutil in two distinct files. | 2016-03-20 | |
* | | | Pushing Proofview further down the dependency alley. | 2016-03-20 | |
* | | | Moving Refine to its proper module. | 2016-03-20 | |
* | | | Do not export entry_key from Pcoq anymore. | 2016-03-19 | |
* | | | Simplifying the code of Entry. | 2016-03-19 | |
* | | | Merge branch 'v8.5' | 2016-03-18 | |
|\ \ \ | | |/ | |/| | |||
* | | | Documenting the change of EXTEND macros. | 2016-03-18 | |
| * | | Trying to circumvent hdiutil error 5341 by padding. | 2016-03-14 | |
* | | | Removing an empty file detected by Luc Grateau. | 2016-03-12 | |
* | | | Merge branch 'render-prehistory' of https://github.com/aspiwack/coq into aspi... | 2016-03-09 | |
|\ \ \ | |||
* | | | | Putting Tactic_debug just below Tacinterp. | 2016-03-06 | |
* | | | | Moving Tactic_debug to tactics/ folder. | 2016-03-06 | |
* | | | | Moving Ltac traces to Tacexpr and Tacinterp. | 2016-03-06 | |
* | | | | Fixing bug #4610: Fails to build with camlp4 since the TACTIC EXTEND move. | 2016-03-06 | |
* | | | | Merge branch 'v8.5' | 2016-03-05 | |
|\ \ \ \ | | |/ / | |/| | | |||
| * | | | Rename Ephemeron -> CEphemeron. | 2016-03-04 | |
| * | | | Fix a typo in dev/doc/changes.txt | 2016-03-04 | |
* | | | | CLEANUP: Context.{Rel,Named}.Declaration.t | 2016-02-09 | |
* | | | | Merge branch 'v8.5' | 2016-01-29 | |
|\| | | | |||
| * | | | Compile OS X binaries without native_compute support. | 2016-01-21 | |
* | | | | Merge branch 'v8.5' | 2016-01-21 | |
|\| | | | |||
| * | | | Update copyright headers. | 2016-01-20 | |
* | | | | Removing constr generic argument. | 2016-01-14 | |
* | | | | Merge branch 'v8.5' | 2016-01-13 | |
|\| | | | |||
| * | | | Fixing #4467 (continued). | 2016-01-13 | |
* | | | | merge | 2016-01-11 | |
|\ \ \ \ | |||
| * | | | | CLEANUP: kernel/context.ml{,i} | 2016-01-11 | |
* | | | | | Merge remote-tracking branch 'origin/v8.5' into trunk | 2016-01-06 | |
|\ \ \ \ \ | | |/ / / | |/| | | | |||
| * | | | | Fix order of files in mllib. | 2016-01-05 | |
* | | | | | Simplification of grammar_prod_item type. | 2016-01-02 | |
* | | | | | Finer-grained types for toplevel values. | 2015-12-21 | |
* | | | | | Using dynamic values in tactic evaluation. | 2015-12-21 | |
| |/ / / |/| | | | |||
* | | | | Tying the loop in tactic printing API. | 2015-12-18 | |
* | | | | Merge branch 'v8.5' | 2015-12-08 | |
|\| | | | |||
| * | | | Fixing a minor problem in Makefile.build that was prevening "dev/printers.cma... | 2015-12-07 |