| Age | Commit message (Expand) | Author |
|---|
| 2010-06-22 | New script dev/tools/change-header to automatically update Coq files headers. | herbelin |
| 2010-06-18 | Quick fix for having clenv debug printer working in trunk. | herbelin |
| 2010-06-13 | Fixed bug #2314 (inversion using not checking the correctness of its arguments | herbelin |
| 2010-06-09 | Fix bug #2317: setoid_rewrite ignored binding lists. Slightly | msozeau |
| 2010-06-09 | Automatic introduction of names given before ":" in Lemma's and | herbelin |
| 2010-06-07 | Fix comment | glondu |
| 2010-06-06 | Added support for Ltac-matching terms with variables bound in the pattern | herbelin |
| 2010-05-29 | Typo in comment of proof.ml | 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-10 | 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-05 | Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proof | pboutill |
| 2010-04-29 | 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-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2010-03-08 | Consider OccurCheck a catchable exception. | msozeau |
| 2010-01-28 | New command Declare Reduction <id> := <conv_expr>. | letouzey |
| 2010-01-04 | Errors issued by reduction tactics (e.g. pattern) were not caught by "try". | herbelin |
| 2009-12-30 | Fixing bug #2146 (broken selection of occurrences in "change"). | 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-22 | Attached evar source to the evar_info and add location to tclWITHHOLES errors | herbelin |
| 2009-12-21 | 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-19 | Made the interpretation levels rlevel/glevel/tlevel truly phantom | herbelin |
| 2009-11-27 | Added support for definition of fixpoints using tactics. | herbelin |
| 2009-11-11 | Promote evar_defs to evar_map (in Evd) | glondu |
| 2009-11-09 | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin |
| 2009-11-08 | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin |
| 2009-10-30 | Take constraints into account in the "instantiate" tactic | herbelin |
| 2009-10-28 | Remove old compatibility stuff (Tacred.nf) | glondu |
| 2009-10-27 | fixed czar bug with parametric inductives | corbinea |
| 2009-10-25 | 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-21 | This big commit addresses two problems: | soubiran |
| 2009-09-20 | Only one "in" clause in "destruct" even for a multiple "destruct". | herbelin |
| 2009-09-18 | - Fixed a bug in checking that implicit arguments are all correctly | 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-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-03 | Added "etransitivity". | herbelin |
| 2009-07-15 | - Fixing bug #2139 (kernel-based test of well-formation of elimination | herbelin |
| 2009-07-08 | Reactivation of pattern unification of evars in apply unification, in | herbelin |
| 2009-07-07 | Jolification : tentative de supprimer les "( evd)" et associés qui | aspiwack |
| 2009-06-11 | Use a lazy value for the message in FailError, so that it won't be | msozeau |
| 2009-06-06 | Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0 | herbelin |
