| Commit message (Expand) | Author | Age |
|---|
| * | Fix inductive_template building ill-typed evars, and update test-suite scripts |  msozeau | 2011-03-13 |
| * | - Add modulo_delta_types flag for unification to allow full | msozeau | 2011-03-13 |
| * | Keep information on which fields are subclasses in class declarations, | msozeau | 2011-03-11 |
| * | 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 |
| * | Forgot a use of evars_reset_evd in nf_evars, add an optional argument as | msozeau | 2011-03-10 |
| * | Do not forget conv_pbs when resetting an evm: | msozeau | 2011-03-10 |
| * | Solve evar instantiations in the right environment. | msozeau | 2011-03-08 |
| * | Reverted commit r13893 about propagation of more informative |  herbelin | 2011-03-07 |
| * | Revert commit r13883: instantiating ?n by a lambda when "?n a" has to | 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 |
| * | A few more betaiota on environments and types of error messages. Seems to | herbelin | 2011-03-05 |
| * | Added support for instantiation of ?n by a lambda when "?n a" has to | herbelin | 2011-03-05 |
| * | Reorganized a bit evarconv.ml: | 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 |
| * | - Use transparency information all the way through unification and | msozeau | 2011-02-17 |
| * | - Fix treatment of globality flag for typeclass instance hints (they | msozeau | 2011-02-14 |
| * | An automatic substitution of scope at functor application |  letouzey | 2011-02-11 |
| * | 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 |
| * | Make simpl use the proper constant when folding (mutual) fixpoints | letouzey | 2011-01-27 |
| * | ratrapage exception, deja fait ... |  bgregoir | 2011-01-11 |
| * | Fixing an uncaught exception bug with use of vmcast | herbelin | 2011-01-07 |
| * | mli comments for doc |  pboutill | 2011-01-07 |
| * | Rename mkR* smart constructors (mostly in funind) |  glondu | 2010-12-25 |
| * | More {raw => glob} changes for consistency | glondu | 2010-12-24 |
| * | Rename rawterm.ml into glob_term.ml | glondu | 2010-12-23 |
| * | Change of nomenclature: rawconstr -> glob_constr | glondu | 2010-12-23 |
| * | Fixing bug #2454: inversion predicate strategy for inferring the type | herbelin | 2010-12-19 |
| * | Univ.constraints made fully abstract instead of being a Set of abstract stuff | letouzey | 2010-12-18 |
| * | Misc improvements about evar_map | letouzey | 2010-12-15 |
| * | Refresh universes in params when generating schemes (Closes: #2429) | glondu | 2010-11-08 |
| * | Delayed the evar normalization in error messages to the last minute | herbelin | 2010-11-07 |
| * | An experimental support for open constrs in hints and in "using" | herbelin | 2010-10-31 |
| * | Cleaning the use of parentheses around evd and evdref (cosmetic commit). | herbelin | 2010-10-31 |
| * | Slight cosmetic cleaning of tacred.ml. | herbelin | 2010-10-31 |
| * | Fixing the Not_found error in bug #2404 + dead code removal in cases.ml | herbelin | 2010-10-06 |
| * | Improve handling of metas as evars in unification (patch by Hugo) | letouzey | 2010-09-30 |
| * | Speed-up refine by avoiding some calls to Evd.fold | letouzey | 2010-09-30 |
| * | Fix bug #2321, allowing "_" named projections in classes. Not realizing | msozeau | 2010-09-28 |
| * | Remove some occurrences of "open Termops" | glondu | 2010-09-28 |
| * | Remove "init" label from Termops.it_mk* specialized functions | glondu | 2010-09-28 |
| * | Some dead code removal, thanks to Oug analyzer | letouzey | 2010-09-24 |
| * | Added eta-expansion in kernel, type inference and tactic unification, | herbelin | 2010-09-20 |
| * | Improving a few error messages in Ltac interpretation | herbelin | 2010-09-11 |
| * | Fix [clenv_missing] to compute a better approximation of missing | msozeau | 2010-08-02 |
| * | kernel conversion and reduction do not raise assert failure on ill-typed term... |  barras | 2010-07-29 |
| * | fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate... | barras | 2010-07-29 |
msozeau
herbelin
letouzey
bgregoir
pboutill
glondu
barras