| Age | Commit message (Expand) | Author |
|---|
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-06-01 | Getting rid of Pp.msgnl and Pp.message. | ppedrot |
| 2012-05-31 | tactic is_fix, akin to is_evar, is_hyp, is_ ... family | pboutill |
| 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 | Basic stuff about constr_expr migrated from topconstr to constrexpr_ops | 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 | Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd | letouzey |
| 2012-04-17 | Remove the Dp plugin. | gmelquio |
| 2012-03-14 | Second step of integration of Program: | msozeau |
| 2012-03-02 | Noise for nothing | pboutill |
| 2012-02-07 | A "Grab Existential Variables" to transform the unresolved evars at the end o... | aspiwack |
| 2011-11-17 | Merge subinstances branch by me and Tom Prince. | msozeau |
| 2011-11-02 | Add type annotations around all calls to Libobject.declare_object | letouzey |
| 2011-10-07 | A new tactic is_var to check whether a term is a goal/section variable | letouzey |
| 2011-09-26 | Moving implicit tactic support from Tacinterp to Pfedit and final evar | herbelin |
| 2011-06-18 | Relaxed the constraint introduced in r14190 that froze the existing | herbelin |
| 2011-02-14 | - Fix treatment of globality flag for typeclass instance hints (they | msozeau |
| 2010-12-27 | Rename the "raw" argument extension into "glob" | glondu |
| 2010-12-24 | More {raw => glob} changes for consistency | glondu |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-12-23 | Change of nomenclature: rawconstr -> glob_constr | glondu |
| 2010-12-02 | Add tactic has_evar (#2433) | glondu |
| 2010-12-02 | Add tactic is_evar (Closes: #2433) | glondu |
| 2010-11-07 | Delayed the evar normalization in error messages to the last minute | herbelin |
| 2010-09-30 | Simplify tactic(_)-bound arguments in TACTIC EXTEND rules | glondu |
| 2010-09-28 | Remove some occurrences of "open Termops" | glondu |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-07-22 | Adding the destauto tactic, that reduces match by destructing matched | courtieu |
| 2010-07-09 | Finish adding out-of-the-box support for camlp4 | letouzey |
| 2010-06-28 | Made "replace" accepts open terms on its left-hand-side. | herbelin |
| 2010-06-22 | Added Chung-Kil Hur's smart "pattern" tactic (h_resolve). | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-01-30 | Update CHANGES, add documentation for new commands/tactics and do a bit | msozeau |
| 2009-12-21 | Generic support for open terms in tactics | herbelin |
| 2009-12-12 | Updated compatibility for rewriting equality proofs that are dependent | herbelin |
| 2009-11-24 | Minor fixes in typeclasses, avoiding repeated evar normalizations. | msozeau |
| 2009-10-28 | Integrate a few improvements on typeclasses and Program from the equations br... | msozeau |
| 2009-10-21 | This big commit addresses two problems: | soubiran |
| 2009-09-17 | Remove useless Liboject.export_function field | glondu |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-08-13 | Death of "survive_module" and "survive_section" (the first one was | herbelin |
| 2009-08-06 | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | herbelin |
| 2009-08-06 | Move out JMeq of subst for compatibility (it affects e.g. the | herbelin |
| 2009-07-24 | Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite" | letouzey |
| 2009-06-30 | Add new variants of [rewrite] and [autorewrite] which differ in the | msozeau |
| 2009-05-20 | - Fixing declarative mode in presence of high use of Change_evars nodes | herbelin |
| 2009-05-09 | - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence | herbelin |
