| Age | Commit message (Expand) | Author |
| 2013-09-26 | Splitting Rewrite into a code part and a CAMLP4-dependent one. | ppedrot |
| 2013-09-18 | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot |
| 2013-08-08 | get rid of closures in global/proof state | gareuselesinge |
| 2013-08-08 | Vernac classification streamlined (handles VERNAC EXTEND) | gareuselesinge |
| 2013-08-08 | State Transaction Machine | gareuselesinge |
| 2013-07-17 | Pre-create typeclass_instances and rewrite hintdb in Auto | letouzey |
| 2013-06-22 | Now, idtac closures use maps instead of association list. | ppedrot |
| 2013-06-21 | Cutting the dependency of Genarg in constr_expr, glob_constr | ppedrot |
| 2013-06-19 | - Keep the refinement of existing evars comming from unification with a rewri... | msozeau |
| 2013-06-14 | Using an "extra" Store.t field in interp_sign instead of dedicated | ppedrot |
| 2013-06-14 | When doing setoid_rewrite through rewrite, do resolution of classes | msozeau |
| 2013-06-12 | Fixing a Not_found and evar not found anomaly found in ATBR, | msozeau |
| 2013-06-12 | One more fix for rewrite: disallow resolving of the (partial) constraints | msozeau |
| 2013-06-10 | Fix [setoid_rewrite] forgetting some evars that are produced when typecheckin... | msozeau |
| 2013-06-07 | Cleanup in rewrite.ml4, remove Evd.merge... replaced by an evars_reset_evd | msozeau |
| 2013-06-06 | Uniformizing generic argument types. | ppedrot |
| 2013-06-04 | Start documenting new [rewrite_strat] tactic that applies rewriting | msozeau |
| 2013-05-12 | Use the Hook module here and there. | ppedrot |
| 2013-05-09 | Uniformization: isevars -> evdref/sigma/evd | herbelin |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-04-15 | anew_instance should not consume the locality twice | gareuselesinge |
| 2013-04-15 | More functional implementation of locality_flag and program_mode | gareuselesinge |
| 2013-03-22 | Fix bug# 2994, 2971 about better error messages. | msozeau |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 13) | letouzey |
| 2013-03-12 | invalid_arg instead of raise (Invalid_argement ...) | letouzey |
| 2013-02-19 | Dir_path --> DirPath | letouzey |
| 2013-02-18 | Removing Exc_located and using the new exception enrichement | ppedrot |
| 2013-02-18 | Minor code cleanups, especially take advantage of Dir_path.is_empty | letouzey |
| 2013-01-28 | Actually adding backtrace handling. | ppedrot |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-12-18 | Fixed a little inefficiency of "set/destruct" over a pattern. Now | herbelin |
| 2012-12-14 | Modulification of dir_path | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-11-25 | Monomorphization (tactics) | ppedrot |
| 2012-10-16 | Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp | letouzey |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-09-18 | More cleaning in CArray... | ppedrot |
| 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-07-11 | Fix typeclass error handling which was sometimes raising a Failure ("hd"). | msozeau |
| 2012-07-10 | Better treatment of error messages in rewrite (avoid use of Errors.print). | msozeau |
| 2012-07-05 | rewrite_db : a first attempt at using rewrite_strat for a quicker autorewrite | letouzey |
| 2012-07-05 | Fixes in rewriting by strategies (almost ready to be documented!): | msozeau |
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-06-19 | Fix bug #2790: wrong handling of Set -> Prop -> Prop products in setoid rewri... | msozeau |
| 2012-05-30 | Getting rid of Pp.msg | ppedrot |
| 2012-05-29 | place all files specific to camlp4 syntax extensions in grammar/ | letouzey |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |