| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2011-09-12 | Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the... | aspiwack |
| 2011-08-30 | Porting Hendrik's 8.3 patch for proof tree visualization under proof | herbelin |
| 2011-06-21 | Cleaning debugging printer relative to new proof engine. In | herbelin |
| 2011-05-13 | The modules in proofs now use the Errors module to explain their exceptions t... | aspiwack |
| 2011-02-07 | Factorize code of rewrite to make way for a new implementation using the | msozeau |
| 2010-12-23 | Change of nomenclature: rawconstr -> glob_constr | glondu |
| 2010-12-13 | Goal: preventively replace an Evd.fold by an equivalent Evd.fold_undefined | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2007-10-23 | Enlevé les trucs commités au mauvais endroit | aspiwack |
| 2007-10-23 | Quelques structures de donnée plus les modules principaux (et | aspiwack |
