| Commit message (Expand) | Author | Age |
|---|
| * | Fix nf_evars_undefined |  msozeau | 2011-08-03 |
| * | Evarutil: replace generic list_distinct on constr by constr_list_distinct |  puech | 2011-07-29 |
| * | Evarutil: replaced some generic = on constr by destructors | puech | 2011-07-29 |
| * | Evarutil: generic equality on constr replaced by destructors | puech | 2011-07-29 |
| * | Evarutil: generic equality on constr replaced by eq_constr (x2) | puech | 2011-07-29 |
| * | Evarutil: generic equality on constr replaced by eq_constr | puech | 2011-07-29 |
| * | Added full pattern-unification on Meta for tactic unification. |  herbelin | 2011-06-13 |
| * | Fixes in pruning, do not fail if pruning is impossible due to typing constrai... | msozeau | 2011-06-10 |
| * | More fixes in pruning/restriction of evars during unification. | msozeau | 2011-06-09 |
| * | Fixes in pruning in unification. | msozeau | 2011-06-08 |
| * | - Fix restrict_hyps to not allow filtering on a variable required to typechec... | msozeau | 2011-06-07 |
| * | - Make typeclass transparency information directly available | msozeau | 2011-04-13 |
| * | - Remove create_evar_defs | msozeau | 2011-04-13 |
| * | Catch NotArity exception and transform it into an anomaly in retyping. | msozeau | 2011-04-11 |
| * | - Fix solve_simpl_eqn which was cheking instances types in the wrong environm... | msozeau | 2011-03-23 |
| * | Tentative to make unification check types at every instanciation of an | msozeau | 2011-03-11 |
| * | - Better error messages taking unif. constraints into account. | msozeau | 2011-03-11 |
| * | Reverted commit r13893 about propagation of more informative | herbelin | 2011-03-07 |
| * | Added propagation of evars unification failure reasons for better | herbelin | 2011-03-07 |
| * | Added a table for using reserved names for binding names to types | herbelin | 2011-03-05 |
| * | Improved define_evar_as_lambda which was creating an unrelated new evar | herbelin | 2011-03-05 |
| * | Instantiate evar by a lambda when "?n args" has to unify with Prod | herbelin | 2011-03-05 |
| * | In evars_of_term and co, visit array c in Evar(_,c) (sequel to r13809) |  letouzey | 2011-02-11 |
| * | Repair Class_tactics.split_evars, broken by r13717 (should fix #2481) | letouzey | 2011-02-03 |
| * | Rename rawterm.ml into glob_term.ml |  glondu | 2010-12-23 |
| * | Speed-up refine by avoiding some calls to Evd.fold | letouzey | 2010-09-30 |
| * | Some dead code removal, thanks to Oug analyzer | letouzey | 2010-09-24 |
| * | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
| * | Fix (part of) bug #2347, de Bruijn bug in Program's pretyper. | msozeau | 2010-06-30 |
| * | Made tclABSTRACT normalize evars before saying it does not support | herbelin | 2010-06-29 |
| * | Added rudimentary support for using constructors from the explicit | herbelin | 2010-06-12 |
| * | Fixed a bug in evarutil.ml (wrong env of a postponed conversion problem). | herbelin | 2010-06-12 |
| * | Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic). | herbelin | 2010-06-11 |
| * | Fixing Derive Inversion for new proof engine | herbelin | 2010-05-26 |
| * | Improved the efficiency of evars traverals thanks to a split of | herbelin | 2010-05-13 |
| * | 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 |
| * | Fixed bugs from commit 12954 on unification complexity | herbelin | 2010-04-20 |
| * | Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2). | herbelin | 2010-04-19 |
| * | 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 |
| * | 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 |
| * | Reverted an incorrect code simplification in function status_changed | herbelin | 2009-11-02 |
| * | Take constraints into account in the "instantiate" tactic | herbelin | 2009-10-30 |
| * | Integrate a few improvements on typeclasses and Program from the equations br... | msozeau | 2009-10-28 |
| * | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
| * | Made unification patch 12268 even more ad hoc (if evars remain in a | herbelin | 2009-08-13 |
| * | Relatively ad hoc fix to an ill-typed instantiation bug in type | herbelin | 2009-08-11 |
| * | Don't use recent ocaml tolerance for pattern "ProjectVar _" when | herbelin | 2009-07-08 |
msozeau
puech
herbelin
letouzey
glondu
aspiwack