| Commit message (Expand) | Author | Age |
|---|
| * | 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 |
| * | Add new variants of [rewrite] and [autorewrite] which differ in the |  msozeau | 2009-06-30 |
| * | Use a lazy value for the message in FailError, so that it won't be | msozeau | 2009-06-11 |
| * | - Added two new introduction patterns with the following temptative syntaxes: | herbelin | 2009-06-07 |
| * | - Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: it | herbelin | 2009-05-10 |
| * | - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence | herbelin | 2009-05-09 |
| * | - 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-27 |
| * | Fixing bug #2308 ("instantiate" tactic did not comply with | herbelin | 2009-04-24 |
| * | nouvelle version de la tactique groebner proposee par Loic: |  barras | 2009-04-16 |
| * | Display the content of the list instead of "<list>" when an idtac | herbelin | 2009-04-05 |
| * | Fix useless redeclaration of a tactic name when UpdateTac is replayed. | msozeau | 2009-03-28 |
| * | Backport from v8.2 branch of 11986 (interpretation of quantified | herbelin | 2009-03-22 |
| * | coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ... | barras | 2009-03-19 |
| * | - gros commit sur ring et field: passage des arguments simplifie | barras | 2009-03-17 |
| * | 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 | 2009-03-04 |
| * | =?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=... | aspiwack | 2009-02-27 |
| * | On remplace evar_map par evar_defs (seul evar_defs est désormais exporté | aspiwack | 2009-02-19 |
| * | Fixed bugs #2001 (search_guard was overwriting the guard index given | herbelin | 2009-01-04 |
| * | - Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H", | herbelin | 2009-01-02 |
| * | - Added support for subterm matching in SearchAbout. | herbelin | 2008-12-29 |
| * | About "apply in": | herbelin | 2008-12-09 |
| * | Port [rewrite] tactics to open terms. Currently no check that evars | msozeau | 2008-11-05 |
| * | More debugging of handling of open constrs with typeclasses: | msozeau | 2008-10-25 |
| * | Forgot one file which had other local modifications... | msozeau | 2008-10-23 |
| * | - Export de pattern_ident vers les ARGUMENT EXTEND and co. | herbelin | 2008-10-19 |
| * | Optimisation de clenv.ml pour que meta_instance ne soit pas appelé | herbelin | 2008-10-18 |
herbelin
glondu
soubiran
gmelquio
aspiwack
msozeau
barras