| Age | Commit message (Expand) | Author |
|---|
| 2014-12-16 | Getting rid of Exninfo hacks. | Pierre-Marie Pédrot |
| 2014-12-07 | Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic. | Hugo Herbelin |
| 2014-11-16 | Fixing side bug in db37c9f3f32ae7 delaying interpretation of the | Hugo Herbelin |
| 2014-10-15 | Remaining tactics of the Auto module were put in the monad. | Pierre-Marie Pédrot |
| 2014-10-09 | A version of convert_concl and convert_hyp in new proof engine. | Hugo Herbelin |
| 2014-10-07 | Splitting out of auto.ml a file hints.ml dedicated to hints so as to | Hugo Herbelin |
| 2014-10-02 | Fixing bug #2810 (autounfold on local variable declared as hint but cleared). | Hugo Herbelin |
| 2014-09-15 | Add a "Hint Mode ref (+ | -)*" hint for setting a global mode | Matthieu Sozeau |
| 2014-09-10 | A step towards better differentiating when w_unify is used for subterm | Hugo Herbelin |
| 2014-08-23 | Tactics.unify in the new monad. | Pierre-Marie Pédrot |
| 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 |
