| Commit message (Expand) | Author | Age |
* | Fix compilation broken by Matthieu's last commit. | Pierre Letouzey | 2015-04-10 |
* | Eauto hints respect their priority. Fixes bug #3199. | Pierre-Marie Pédrot | 2015-04-10 |
* | Fixing bug #3298. | Pierre-Marie Pédrot | 2015-02-26 |
* | Update headers. | Maxime Dénès | 2015-01-12 |
* | Getting rid of Exninfo hacks. | Pierre-Marie Pédrot | 2014-12-16 |
* | Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic. | Hugo Herbelin | 2014-12-07 |
* | Fixing side bug in db37c9f3f32ae7 delaying interpretation of the | Hugo Herbelin | 2014-11-16 |
* | Remaining tactics of the Auto module were put in the monad. | Pierre-Marie Pédrot | 2014-10-15 |
* | A version of convert_concl and convert_hyp in new proof engine. | Hugo Herbelin | 2014-10-09 |
* | Splitting out of auto.ml a file hints.ml dedicated to hints so as to | Hugo Herbelin | 2014-10-07 |
* | Fixing bug #2810 (autounfold on local variable declared as hint but cleared). | Hugo Herbelin | 2014-10-02 |
* | Add a "Hint Mode ref (+ | -)*" hint for setting a global mode | Matthieu Sozeau | 2014-09-15 |
* | A step towards better differentiating when w_unify is used for subterm | Hugo Herbelin | 2014-09-10 |
* | Tactics.unify in the new monad. | Pierre-Marie Pédrot | 2014-08-23 |
* | Reorganization of tactics: | Hugo Herbelin | 2014-08-18 |
* | Correct eauto which was not dealing properly with polymorphic constants. | Matthieu Sozeau | 2014-07-21 |
* | Properly refresh the local hintdb database in case an external tactic changed | Matthieu Sozeau | 2014-06-26 |
* | Clenvtac.unify is in the new monad. | Pierre-Marie Pédrot | 2014-06-23 |
* | Oops, I fixed the .ml's | Matthieu Sozeau | 2014-06-23 |
* | Removing dead code. | Pierre-Marie Pédrot | 2014-06-17 |
* | Passing some tactics to the new monad type. | Pierre-Marie Pédrot | 2014-06-12 |
* | Now parsing rules of ML-declared tactics are only made available after the | Pierre-Marie Pédrot | 2014-05-12 |
* | - 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-05-06 |
* | Removing dead code, thanks to new OCaml warnings and a bit of scripting. | Pierre-Marie Pédrot | 2014-04-23 |
* | Closing bug #3260 | Julien Forest | 2014-04-14 |
* | Removing unused functions in Refiner. | Pierre-Marie Pédrot | 2014-04-06 |
* | Fixing bug #3226. | Pierre-Marie Pédrot | 2014-02-02 |
* | Remove the Hiddentac module. | Arnaud Spiwack | 2013-11-25 |
* | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack | 2013-11-02 |
* | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc | 2013-09-19 |
* | Some cleanup in Auto | ppedrot | 2013-09-03 |
* | Vernac classification streamlined (handles VERNAC EXTEND) | gareuselesinge | 2013-08-08 |
* | More functional implementation of locality_flag and program_mode | gareuselesinge | 2013-04-15 |
* | Restrict (try...with...) to avoid catching critical exn (part 13) | letouzey | 2013-03-13 |
* | Modulification of Label | ppedrot | 2012-12-18 |
* | Modulification of identifier | ppedrot | 2012-12-14 |
* | Monomorphization (tactics) | ppedrot | 2012-11-25 |
* | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey | 2012-10-02 |
* | 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-09-14 |
* | Updating headers. | herbelin | 2012-08-08 |
* | More cleaning | ppedrot | 2012-06-01 |
* | 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-05-29 |
* | Remove print call that do not use the pp mechanism | pboutill | 2012-04-12 |
* | info_trivial, info_auto, info_eauto, and debug (trivial|auto) | letouzey | 2012-03-30 |