| Commit message (Expand) | Author | Age |
|---|
| * | Revert r14078 "Partial backtrack on the support for open terms in destruct/in... |  gmelquio | 2011-04-28 |
| * | Partial backtrack on the support for open terms in destruct/induction: | gmelquio | 2011-04-28 |
| * | More informative anomaly. |  herbelin | 2011-04-14 |
| * | Revert "Add [Polymorphic] flag for defs" |  msozeau | 2011-04-13 |
| * | - Remove create_evar_defs | msozeau | 2011-04-13 |
| * | Add [Polymorphic] flag for defs | msozeau | 2011-04-13 |
| * | A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> seconds |  letouzey | 2011-03-18 |
| * | Rename subst_raw_with_bindings to subst_glob_with_bindings and export | msozeau | 2011-02-10 |
| * | Rename rawterm.ml into glob_term.ml |  glondu | 2010-12-23 |
| * | Change of nomenclature: rawconstr -> glob_constr | glondu | 2010-12-23 |
| * | An experimental support for open constrs in hints and in "using" | herbelin | 2010-10-31 |
| * | Some dead code removal, thanks to Oug analyzer | letouzey | 2010-09-24 |
| * | Improving a few error messages in Ltac interpretation | herbelin | 2010-09-11 |
| * | Capitulation wrt "change pat with term": instead of solving the | herbelin | 2010-07-30 |
| * | oops. commited files I shouldn't have. reverting on r13341 |  barras | 2010-07-28 |
| * | ported r13340 to trunk | barras | 2010-07-28 |
| * | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
| * | Fixed a bug introduced in a combination in r12807 and revealed in | herbelin | 2010-06-28 |
| * | Fixed commit 13125 (stricter check of induction args): an interpretation | herbelin | 2010-06-14 |
| * | Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes). | herbelin | 2010-06-13 |
| * | Made intros_until and onInductionArg a bit stricter and robust | herbelin | 2010-06-13 |
| * | Fixed a bug in pretty-printing "induction" and "destruct" due to a | herbelin | 2010-06-13 |
| * | Added support for Ltac-matching terms with variables bound in the pattern | herbelin | 2010-06-06 |
| * | Add (almost) compatibility with camlp4, without breaking support for camlp5 | letouzey | 2010-05-19 |
| * | Improved the efficiency of evars traverals thanks to a split of | herbelin | 2010-05-13 |
| * | term matching in ltac was not coherent with match goal in presence of wildcar... |  jforest | 2010-05-06 |
| * | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
| * | Here comes the commit, announced long ago, of the new tactic engine. |  aspiwack | 2010-04-22 |
| * | Fixing bug #2146 (broken selection of occurrences in "change"). | herbelin | 2009-12-30 |
| * | Safer, though ad hoc, approach to re-interpretation of the argument of | herbelin | 2009-12-28 |
| * | In "simpl c" and "change c with d", c can be a pattern. | herbelin | 2009-12-24 |
| * | Opened the possibility to type Ltac patterns but it is not fully functional yet | herbelin | 2009-12-24 |
| * | Moved a bit further the code for pattern interpretation in match goal | herbelin | 2009-12-23 |
| * | Generic support for open terms in tactics | herbelin | 2009-12-21 |
| * | Make usage of Dyn explicit | glondu | 2009-10-28 |
| * | New cleaning phase of the Local/Global option management | herbelin | 2009-10-26 |
| * | This big commit addresses two problems: |  soubiran | 2009-10-21 |
| * | Relaxed error severity when encountering unknown library objects or tactic | gmelquio | 2009-10-06 |
| * | Apply "Declare Implicit Tactic" also to terms interpreted as "open | herbelin | 2009-09-27 |
| * | Fixed a hole in glob_tactic that allowed some Ltac code to refer to | herbelin | 2009-09-26 |
| * | Only one "in" clause in "destruct" even for a multiple "destruct". | herbelin | 2009-09-20 |
| * | Remove useless Liboject.export_function field | glondu | 2009-09-17 |
| * | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
| * | Generalized the possibility to refer to a global name by a notation | herbelin | 2009-09-11 |
| * | Added syntax "exists bindings, ..., bindings" for iterated "exists". | herbelin | 2009-09-10 |
| * | Death of "survive_module" and "survive_section" (the first one was | herbelin | 2009-08-13 |
| * | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | herbelin | 2009-08-06 |
| * | - Add more precise error localisation when one of the application fails | herbelin | 2009-08-04 |
| * | Added "etransitivity". | herbelin | 2009-08-03 |
| * | Jolification : tentative de supprimer les "( evd)" et associés qui | aspiwack | 2009-07-07 |
gmelquio
herbelin
msozeau
letouzey
glondu
barras
jforest
aspiwack
soubiran