| Commit message (Expand) | Author | Age |
|---|
| * | 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 |
| * | Fix: Pfedit.get_current_goal_context when no goal is focused. |  aspiwack | 2010-05-10 |
| * | Removed an evar_merge in clenv_fchain which not only is incorrect but | herbelin | 2010-05-10 |
| * | Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proof |  pboutill | 2010-05-05 |
| * | Various minor improvements of comments in mli for ocamldoc | letouzey | 2010-04-29 |
| * | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
| * | Move from ocamlweb to ocamdoc to generate mli documentation | pboutill | 2010-04-29 |
| * | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack | 2010-04-22 |
| * | Consider OccurCheck a catchable exception. |  msozeau | 2010-03-08 |
| * | New command Declare Reduction <id> := <conv_expr>. | letouzey | 2010-01-28 |
| * | Errors issued by reduction tactics (e.g. pattern) were not caught by "try". | herbelin | 2010-01-04 |
| * | Fixing bug #2146 (broken selection of occurrences in "change"). | herbelin | 2009-12-30 |
| * | 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 |
| * | Attached evar source to the evar_info and add location to tclWITHHOLES errors | herbelin | 2009-12-22 |
| * | Generic support for open terms in tactics | herbelin | 2009-12-21 |
| * | In "progress", extending the set of evars w/o solving an existing one is | herbelin | 2009-12-21 |
| * | Made the interpretation levels rlevel/glevel/tlevel truly phantom | herbelin | 2009-12-19 |
| * | Added support for definition of fixpoints using tactics. | herbelin | 2009-11-27 |
| * | Promote evar_defs to evar_map (in Evd) |  glondu | 2009-11-11 |
| * | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin | 2009-11-09 |
| * | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin | 2009-11-08 |
| * | Take constraints into account in the "instantiate" tactic | herbelin | 2009-10-30 |
| * | Remove old compatibility stuff (Tacred.nf) | glondu | 2009-10-28 |
| * | fixed czar bug with parametric inductives |  corbinea | 2009-10-27 |
| * | Add support for remaining side-conditions in "apply in as". | herbelin | 2009-10-25 |
| * | Improved the treatment of Local/Global options (noneffective Local on | herbelin | 2009-10-25 |
| * | This big commit addresses two problems: |  soubiran | 2009-10-21 |
| * | Only one "in" clause in "destruct" even for a multiple "destruct". | herbelin | 2009-09-20 |
| * | - Fixed a bug in checking that implicit arguments are all correctly | herbelin | 2009-09-18 |
| * | Remove useless Liboject.export_function field | glondu | 2009-09-17 |
| * | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
| * | 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 |
| * | Added "etransitivity". | herbelin | 2009-08-03 |
| * | - Fixing bug #2139 (kernel-based test of well-formation of elimination | herbelin | 2009-07-15 |
| * | Reactivation of pattern unification of evars in apply unification, in | herbelin | 2009-07-08 |
| * | Jolification : tentative de supprimer les "( evd)" et associés qui | aspiwack | 2009-07-07 |
| * | Use a lazy value for the message in FailError, so that it won't be | msozeau | 2009-06-11 |
| * | Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0 | herbelin | 2009-06-06 |
| * | Backtrack on experimental unification with sort variables: it requires | msozeau | 2009-06-02 |
| * | A try at using sort variables during unification. Instead of refreshing | msozeau | 2009-05-23 |
| * | - Fixing declarative mode in presence of high use of Change_evars nodes | herbelin | 2009-05-20 |
| * | Minor unification changes: | msozeau | 2009-05-18 |
| * | Fixing bug #2308 ("instantiate" tactic did not comply with | herbelin | 2009-04-24 |
| * | Many changes in the Makefile infrastructure + a beginning of ocamlbuild | letouzey | 2009-03-20 |
| * | Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4" | herbelin | 2009-03-16 |
| * | Cleaning/uniformizing the interface of tacticals.mli | herbelin | 2009-03-14 |
letouzey
herbelin
aspiwack
pboutill
msozeau
glondu
corbinea
soubiran