| Commit message (Expand) | Author | Age |
* | 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 |
* | Add heuristic based on non-linearity of evars to determine whether an | herbelin | 2009-07-08 |
* | Fixing bug 2129 (evar introduced to remember an ambiguous projection | herbelin | 2009-07-08 |
* | Jolification : tentative de supprimer les "( evd)" et associés qui | aspiwack | 2009-07-07 |
* | documented a bug of pattern unification with metas | barras | 2009-06-22 |
* | A try at using sort variables during unification. Instead of refreshing | msozeau | 2009-05-23 |
* | - Fixing #2090 (occur check missing when trying to solve evar-evar equation). | herbelin | 2009-04-25 |
* | Some dead code removal + cleanups | letouzey | 2009-04-08 |
* | - Fixing bug #2084 (unification not checking sort constraints), hoping | herbelin | 2009-04-08 |
* | Fix obvious bug in evars_of_named_context. | msozeau | 2009-04-03 |
* | Fixes to make Ynot compile with the trunk: | msozeau | 2009-03-20 |
* | 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 passe les last_mods (un des champs de Evd.evar_defs) de list | aspiwack | 2009-02-20 |
* | On remplace evar_map par evar_defs (seul evar_defs est désormais exporté | aspiwack | 2009-02-19 |
* | memoized is_ground_env | barras | 2009-02-09 |
* | pushed evar reduction in kernel | barras | 2009-02-06 |
* | From v8.2 to trunk: | herbelin | 2009-02-06 |
* | - Fixing bug 1891 (abusive instantiations of evar arguments in | herbelin | 2009-01-20 |
* | Backporting from v8.2 to trunk: | herbelin | 2009-01-18 |