| Age | Commit message (Expand) | Author |
|---|
| 2010-06-28 | Fixed a bug introduced in a combination in r12807 and revealed in | herbelin |
| 2010-06-14 | Fixed commit 13125 (stricter check of induction args): an interpretation | herbelin |
| 2010-06-13 | 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-06 | Added support for Ltac-matching terms with variables bound in the pattern | herbelin |
| 2010-05-19 | Add (almost) compatibility with camlp4, without breaking support for camlp5 | letouzey |
| 2010-05-13 | Improved the efficiency of evars traverals thanks to a split of | herbelin |
| 2010-05-06 | term matching in ltac was not coherent with match goal in presence of wildcar... | jforest |
| 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 |
| 2009-12-30 | Fixing bug #2146 (broken selection of occurrences in "change"). | herbelin |
| 2009-12-28 | Safer, though ad hoc, approach to re-interpretation of the argument of | herbelin |
| 2009-12-24 | 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-23 | Moved a bit further the code for pattern interpretation in match goal | herbelin |
| 2009-12-21 | Generic support for open terms in tactics | herbelin |
| 2009-10-28 | Make usage of Dyn explicit | glondu |
| 2009-10-26 | New cleaning phase of the Local/Global option management | herbelin |
| 2009-10-21 | This big commit addresses two problems: | soubiran |
| 2009-10-06 | Relaxed error severity when encountering unknown library objects or tactic | gmelquio |
| 2009-09-27 | Apply "Declare Implicit Tactic" also to terms interpreted as "open | herbelin |
| 2009-09-26 | Fixed a hole in glob_tactic that allowed some Ltac code to refer to | herbelin |
| 2009-09-20 | Only one "in" clause in "destruct" even for a multiple "destruct". | herbelin |
| 2009-09-17 | Remove useless Liboject.export_function field | glondu |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-09-11 | Generalized the possibility to refer to a global name by a notation | herbelin |
| 2009-09-10 | Added syntax "exists bindings, ..., bindings" for iterated "exists". | herbelin |
| 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-04 | - Add more precise error localisation when one of the application fails | herbelin |
| 2009-08-03 | Added "etransitivity". | herbelin |
| 2009-07-07 | Jolification : tentative de supprimer les "( evd)" et associés qui | aspiwack |
| 2009-06-30 | Add new variants of [rewrite] and [autorewrite] which differ in the | msozeau |
| 2009-06-11 | Use a lazy value for the message in FailError, so that it won't be | msozeau |
| 2009-06-07 | - Added two new introduction patterns with the following temptative syntaxes: | herbelin |
| 2009-05-10 | - Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: it | herbelin |
| 2009-05-09 | - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence | herbelin |
| 2009-04-27 | - Fixed a little bug in previous commit (bad failure in case of unknown entry). | herbelin |
| 2009-04-27 | - Cleaning (unification of ML names, removal of obsolete code, | herbelin |
| 2009-04-24 | Fixing bug #2308 ("instantiate" tactic did not comply with | herbelin |
| 2009-04-16 | nouvelle version de la tactique groebner proposee par Loic: | barras |
| 2009-04-05 | Display the content of the list instead of "<list>" when an idtac | herbelin |
| 2009-03-28 | Fix useless redeclaration of a tactic name when UpdateTac is replayed. | msozeau |
| 2009-03-22 | Backport from v8.2 branch of 11986 (interpretation of quantified | herbelin |
| 2009-03-19 | coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ... | barras |
| 2009-03-17 | - gros commit sur ring et field: passage des arguments simplifie | barras |
| 2009-03-04 | illegal tactic application was having Ltac interpreter loop | barras |
| 2009-03-04 | commande Timeout + compaction des traces de debug_tactic | barras |
| 2009-03-04 | Backtrack sur la mémoïsation de nf_evar. | aspiwack |
