| Age | Commit message (Expand) | Author |
|---|
| 2013-02-18 | Minor code cleanups, especially take advantage of Dir_path.is_empty | letouzey |
| 2013-02-17 | Added propagation of evars unification failure reasons for better | herbelin |
| 2013-02-10 | Useless use of hooks in VernacDefinition. In addition, this was | ppedrot |
| 2013-01-29 | No reason a priori for using unfiltered env for printing | herbelin |
| 2013-01-29 | Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env | herbelin |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2013-01-27 | Avoid failure in debugger when printing Ltac names. | herbelin |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-12-21 | Yet a new reduction tactic in Coq : cbn | pboutill |
| 2012-12-18 | Modulification of name | ppedrot |
| 2012-12-18 | Modulification of mod_bound_id | ppedrot |
| 2012-12-18 | Modulification of Label | ppedrot |
| 2012-12-14 | Modulification of dir_path | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-12-14 | Moved Stringset and Stringmap to String namespace. | ppedrot |
| 2012-12-14 | Moved Intset and Intmap to Int namespace. | ppedrot |
| 2012-11-21 | Print univ constraints generated by a constant or inductive (when flag is set) | barras |
| 2012-11-20 | Cleaning and small optimization in CList. | ppedrot |
| 2012-11-13 | Added a CString module. | ppedrot |
| 2012-11-08 | Monomorphized a lot of equalities over OCaml integers, thanks to | ppedrot |
| 2012-10-31 | Change [Hints Resolve] to still accept constrs as arguments | msozeau |
| 2012-10-29 | Fixed #2926: | ppedrot |
| 2012-10-26 | Change Hint Resolve, Immediate to take a global reference as argument | msozeau |
| 2012-10-16 | Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp | 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 : removal of Proof_type.tactic_expr | letouzey |
| 2012-10-06 | Clean-up : no more Proof_type.proof_tree | letouzey |
| 2012-10-06 | Clean-up of proof_type.ml : no more Nested nor abstract_tactic_box | letouzey |
| 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-10-01 | Added a new tactical infoH tac, that displays the names of hypothesis created... | courtieu |
| 2012-09-20 | Fixing Show Script issues. | 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-08-24 | correct some ends of .mllib files (avoid a broken tolink.ml) | letouzey |
| 2012-08-11 | Added support for option Local (at module level) in Tactic Notation. | herbelin |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-08-07 | Avoid Pp.std_ppcmds in Misctypes.sort_info | letouzey |
| 2012-07-30 | Bigint: avoid dependency over Pp | letouzey |
| 2012-07-21 | Slight modification to the printing of goals when in emacs mode. | courtieu |
| 2012-07-20 | Fixing test-suite | pboutill |
| 2012-07-19 | Getting rid of the undocumented [complete] tactic, which was | ppedrot |
| 2012-07-11 | A friendlier printing of remaining goals when no goal is focused. | aspiwack |
| 2012-07-10 | Fixing Print Assumption display | ppedrot |
| 2012-07-10 | Small change in the printing of proofs for use by coqide. | aspiwack |
