| Age | Commit message (Expand) | Author |
|---|
| 2014-08-18 | Reorganization of tactics: | Hugo Herbelin |
| 2014-07-21 | Correct eauto which was not dealing properly with polymorphic constants. | Matthieu Sozeau |
| 2014-06-26 | Properly refresh the local hintdb database in case an external tactic changed | Matthieu Sozeau |
| 2014-06-23 | Clenvtac.unify is in the new monad. | Pierre-Marie Pédrot |
| 2014-06-23 | Oops, I fixed the .ml's | Matthieu Sozeau |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-06-12 | Passing some tactics to the new monad type. | Pierre-Marie Pédrot |
| 2014-05-12 | Now parsing rules of ML-declared tactics are only made available after the | Pierre-Marie Pédrot |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-23 | Removing dead code, thanks to new OCaml warnings and a bit of scripting. | Pierre-Marie Pédrot |
| 2014-04-14 | Closing bug #3260 | Julien Forest |
| 2014-04-06 | Removing unused functions in Refiner. | Pierre-Marie Pédrot |
| 2014-02-02 | Fixing bug #3226. | Pierre-Marie Pédrot |
| 2013-11-25 | Remove the Hiddentac module. | Arnaud Spiwack |
| 2013-11-02 | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack |
| 2013-09-19 | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc |
| 2013-09-03 | Some cleanup in Auto | ppedrot |
| 2013-08-08 | Vernac classification streamlined (handles VERNAC EXTEND) | gareuselesinge |
| 2013-04-15 | More functional implementation of locality_flag and program_mode | gareuselesinge |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 13) | letouzey |
| 2012-12-18 | Modulification of Label | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-11-25 | Monomorphization (tactics) | ppedrot |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-09-14 | As r15801: putting everything from Util.array_* to CArray.*. | ppedrot |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-06-01 | More cleaning | ppedrot |
| 2012-05-29 | place all files specific to camlp4 syntax extensions in grammar/ | letouzey |
| 2012-05-29 | Pattern as a mli-only file, operations in Patternops | letouzey |
| 2012-05-29 | Glob_term now mli-only, operations now in Glob_ops | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-05-29 | Vernacexpr is now a mli-only file, locality stuff now in locality.ml | letouzey |
| 2012-04-12 | Remove print call that do not use the pp mechanism | pboutill |
| 2012-03-30 | info_trivial, info_auto, info_eauto, and debug (trivial|auto) | letouzey |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-11-17 | Merge subinstances branch by me and Tom Prince. | msozeau |
| 2011-09-23 | auto with nocore : disable the use of the core database (wish #2188) | letouzey |
| 2011-06-10 | Moved allow_K to a unification flag | herbelin |
| 2011-03-11 | - Better error messages taking unif. constraints into account. | msozeau |
| 2011-03-04 | - Allow to set a particular transparent_state for the local hint | msozeau |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-10-31 | An experimental support for open constrs in hints and in "using" | herbelin |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-07-27 | Minor fixes: | msozeau |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-12 | Fixing spelling: pr_coma -> pr_comma | herbelin |
| 2010-06-03 | Avoid computing tactic printing tree (std_ppcmds) when printing not needed in | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
