| Commit message (Expand) | Author | Age |
* | Modulification of identifier | ppedrot | 2012-12-14 |
* | Finish patch for Hint Resolve, stopping to generate new constant names for | msozeau | 2012-12-08 |
* | Monomorphization (tactics) | ppedrot | 2012-11-25 |
* | Change Hint Resolve, Immediate to take a global reference as argument | msozeau | 2012-10-26 |
* | Continue killing hidden tactics : no more generated h_xxx | letouzey | 2012-10-15 |
* | 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 |
* | Updating headers. | herbelin | 2012-08-08 |
* | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot | 2012-06-22 |
* | Getting rid of Pp.msgnl and Pp.message. | ppedrot | 2012-06-01 |
* | tactic is_fix, akin to is_evar, is_hyp, is_ ... family | pboutill | 2012-05-31 |
* | Getting rid of Pp.msg | ppedrot | 2012-05-30 |
* | 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-05-29 |
* | Remove the Dp plugin. | gmelquio | 2012-04-17 |
* | Second step of integration of Program: | msozeau | 2012-03-14 |
* | Noise for nothing | pboutill | 2012-03-02 |
* | A "Grab Existential Variables" to transform the unresolved evars at the end o... | aspiwack | 2012-02-07 |
* | Merge subinstances branch by me and Tom Prince. | msozeau | 2011-11-17 |
* | Add type annotations around all calls to Libobject.declare_object | letouzey | 2011-11-02 |
* | A new tactic is_var to check whether a term is a goal/section variable | letouzey | 2011-10-07 |
* | Moving implicit tactic support from Tacinterp to Pfedit and final evar | herbelin | 2011-09-26 |
* | Relaxed the constraint introduced in r14190 that froze the existing | herbelin | 2011-06-18 |
* | - Fix treatment of globality flag for typeclass instance hints (they | msozeau | 2011-02-14 |
* | Rename the "raw" argument extension into "glob" | glondu | 2010-12-27 |
* | More {raw => glob} changes for consistency | glondu | 2010-12-24 |
* | Rename rawterm.ml into glob_term.ml | glondu | 2010-12-23 |
* | Change of nomenclature: rawconstr -> glob_constr | glondu | 2010-12-23 |
* | Add tactic has_evar (#2433) | glondu | 2010-12-02 |
* | Add tactic is_evar (Closes: #2433) | glondu | 2010-12-02 |
* | Delayed the evar normalization in error messages to the last minute | herbelin | 2010-11-07 |
* | Simplify tactic(_)-bound arguments in TACTIC EXTEND rules | glondu | 2010-09-30 |
* | Remove some occurrences of "open Termops" | glondu | 2010-09-28 |
* | Some dead code removal, thanks to Oug analyzer | letouzey | 2010-09-24 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | Adding the destauto tactic, that reduces match by destructing matched | courtieu | 2010-07-22 |
* | Finish adding out-of-the-box support for camlp4 | letouzey | 2010-07-09 |
* | Made "replace" accepts open terms on its left-hand-side. | herbelin | 2010-06-28 |
* | Added Chung-Kil Hur's smart "pattern" tactic (h_resolve). | herbelin | 2010-06-22 |
* | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
* | Update CHANGES, add documentation for new commands/tactics and do a bit | msozeau | 2010-01-30 |
* | Generic support for open terms in tactics | herbelin | 2009-12-21 |
* | Updated compatibility for rewriting equality proofs that are dependent | herbelin | 2009-12-12 |
* | Minor fixes in typeclasses, avoiding repeated evar normalizations. | msozeau | 2009-11-24 |
* | Integrate a few improvements on typeclasses and Program from the equations br... | msozeau | 2009-10-28 |
* | This big commit addresses two problems: | soubiran | 2009-10-21 |
* | Remove useless Liboject.export_function field | glondu | 2009-09-17 |