| Age | Commit message (Expand) | Author |
|---|
| 2014-04-23 | Better representation of evar filters: we represent the vacuous filters of | Pierre-Marie Pédrot |
| 2014-03-19 | Adding phantom types to discriminate normalized goals, and adding a way to | Pierre-Marie Pédrot |
| 2014-03-07 | Potentially unused computation in Goal. | Pierre-Marie Pédrot |
| 2014-02-27 | Code refactoring thanks to the new Monad module. | Arnaud Spiwack |
| 2014-02-12 | TC: honor the use_typeclasses flag in pretyping | Enrico Tassi |
| 2014-01-10 | Useless Array.of_list | Pierre-Marie Pédrot |
| 2014-01-10 | Exporting the full pretyper options in Goal.constr_of_raw. | Pierre-Marie Pédrot |
| 2013-11-30 | Fixing ltac constr variable handling in refine. | Pierre-Marie Pédrot |
| 2013-11-12 | Useless computation in Goal handle augmentation. | ppedrot |
| 2013-11-09 | Partial applications in Goal. | ppedrot |
| 2013-11-06 | Less partial applications in Vars, as well as better memory allocation. | ppedrot |
| 2013-11-02 | Add primitives in Goal.V82 to access the goal in nf_evar'd form. | aspiwack |
| 2013-11-02 | A tactic shelve_unifiable. | aspiwack |
| 2013-11-02 | Normalise goals with respect to evars in the new tactics. | aspiwack |
| 2013-11-02 | Tachmach.New is now in Proofview.Goal.enter style. | aspiwack |
| 2013-11-02 | A better version of Goal.advance. | aspiwack |
| 2013-11-02 | More optimisations of partial applications. | aspiwack |
| 2013-11-02 | Try to remove intermediate allocations when dealing with goal-specific tactics. | aspiwack |
| 2013-11-02 | A whole new implemenation of the refine tactic. | aspiwack |
| 2013-11-02 | Getting rid of Goal.here, and all the related exceptions and combinators. | aspiwack |
| 2013-11-02 | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack |
| 2013-10-27 | Abstracting evar filter away. The API is not perfect, but better than nothing. | ppedrot |
| 2013-10-24 | More monomorphic List.mem + List.assoc + ... | letouzey |
| 2013-10-05 | Removing dubious use of evarmap manipulating functions in printing | ppedrot |
| 2013-10-05 | Moving side effects into evar_map. There was no reason to keep another | ppedrot |
| 2013-09-18 | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot |
| 2013-09-18 | Removing almost all new_untyped_evar, and a bunch of Evd.add. | ppedrot |
| 2013-08-08 | State Transaction Machine | gareuselesinge |
| 2013-05-09 | A uniformization step around understand_* and interp_* functions. | herbelin |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 12) | letouzey |
| 2013-03-12 | Allowing different types of, not to be mixed, generic Stores through | ppedrot |
| 2013-01-29 | No reason a priori for using unfiltered env for printing | herbelin |
| 2013-01-29 | Fixing bug #2969 (admit failing after Grab Existential Variables due | herbelin |
| 2013-01-29 | Fixed synchronicity of filter with evar context in new_goal_with. | 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 |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-12-13 | Renamed Option.Misc.compare to the more uniform Option.equal. | ppedrot |
| 2012-11-25 | Monomorphization (proof) | ppedrot |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-06-04 | Forward-port fixes from 8.4 (15358, 15353, 15333). | msozeau |
| 2012-05-29 | Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd | letouzey |
| 2012-03-20 | Fix interface of resolve_typeclasses: onlyargs -> with_goals: | msozeau |
| 2012-03-14 | Second step of integration of Program: | msozeau |
| 2012-03-14 | Remove support for "abstract typing constraints" that requires unicity of sol... | msozeau |
| 2012-03-02 | Noise for nothing | pboutill |
| 2012-01-06 | Fixes bug #2654 (tactic instantiate failing to update existential variables). | aspiwack |
| 2011-12-16 | Introducing a notion of evar candidates to be used when an evar is | herbelin |
