| Age | Commit message (Expand) | Author |
|---|
| 2012-11-06 | Coq is a heavy user of persistent data structures and symbolic ASTs, so the | ppedrot |
| 2012-10-29 | Fixed #2926: | ppedrot |
| 2012-10-29 | Removed many calls to OCaml generic equality. This was done by | ppedrot |
| 2012-10-26 | Change Hint Resolve, Immediate to take a global reference as argument | msozeau |
| 2012-10-23 | Text inserted by insert_this_phrase_on_success correct tagging | pboutill |
| 2012-10-17 | Fix test-suite output/* in bench | pboutill |
| 2012-10-17 | univ inconsistency error message gives evidence of a cycle | barras |
| 2012-10-16 | Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp | letouzey |
| 2012-10-14 | When loading a plugin, prefer .cma to .cmo | gareuselesinge |
| 2012-10-06 | Turn mltop.ml4 into a regular ocaml file | letouzey |
| 2012-10-06 | still some more dead code removal | letouzey |
| 2012-10-06 | remove useless hidden_flag in TacMutual(Co)Fix | letouzey |
| 2012-10-06 | Clean-up of proof_type.ml : no more Nested nor abstract_tactic_box | letouzey |
| 2012-10-05 | coqtop -time : display per-command timings | letouzey |
| 2012-10-04 | Improving error message when abtraction over goal (abstract_list_all | herbelin |
| 2012-10-04 | Adding a nominal typing layer to Metasyntax in order to clarify | ppedrot |
| 2012-10-04 | Moved Compat to parsing. This permits to break the dependency of the | ppedrot |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-09-25 | Fixing #2865. | ppedrot |
| 2012-09-18 | More cleaning in CArray... | ppedrot |
| 2012-09-18 | Cleaning interface of Util. | ppedrot |
| 2012-09-17 | More cleaning on Utils and CList. Some parts of the code being | ppedrot |
| 2012-09-15 | Some documentation and cleaning of CList and Util interfaces. | ppedrot |
| 2012-09-14 | As r15801: putting everything from Util.array_* to CArray.*. | ppedrot |
| 2012-09-14 | Partial revert of Yann commit in order to use CLib.List when opening | ppedrot |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-09-14 | This patch removes unused "open" (automatically generated from | regisgia |
| 2012-09-14 | The new ocaml compiler (4.00) has a lot of very cool warnings, | regisgia |
| 2012-09-13 | Made Pp.std_ppcmds opaque. | ppedrot |
| 2012-09-10 | Fixed #2893. | ppedrot |
| 2012-09-09 | When asked for a SearchAbout request, Coq now returns a more precise | ppedrot |
| 2012-09-07 | Avoid [Loading ML file ...] messages when launching coqtop | letouzey |
| 2012-09-06 | Fix computation of obligations for mutually recursive definitions. | msozeau |
| 2012-09-05 | Rationalized the behaviour of "Next Obligation" and "Admit Obligations" | ppedrot |
| 2012-08-24 | Use fully-qualified Coq.Init.Prelude when starting coqtop | letouzey |
| 2012-08-24 | Assumption commands are now displayed as unsafe in Coqide. | aspiwack |
| 2012-08-23 | No more states/initial.coq, instead coqtop now requires Prelude.vo | letouzey |
| 2012-08-22 | Do not forget to build the unicode libraries, necessary to compile and launch... | msozeau |
| 2012-08-11 | Added support for option Local (at module level) in Tactic Notation. | herbelin |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-08-06 | Vecnacentries.dump_global silently ignores exceptions | pboutill |
| 2012-08-05 | Dump references in reduction tactics | pboutill |
| 2012-08-05 | Dump references in Reset | pboutill |
| 2012-07-20 | Fixing test-suite | pboutill |
| 2012-07-20 | Let coqtop be a little more stupid in hint answer: otherwise, that | ppedrot |
| 2012-07-18 | Various minor fixes to coqdoc from A. Chlipala. | msozeau |
| 2012-07-12 | A new status Unsafe in Interface. Meant for commands such as Admitted. | aspiwack |
| 2012-07-12 | Ensure that a plugin init function is called only once | letouzey |
| 2012-07-12 | Vernacentries: minor code cleanup | letouzey |
| 2012-07-12 | Bug 2838: ExplApp in mutual inductive parameters | pboutill |
