| Commit message (Expand) | Author | Age |
* | Allow betaiota when checking unification of the types of metas (fixes ATBR co... | msozeau | 2011-04-20 |
* | Add a flag to control betaiota reduction during unification to maintain backw... | msozeau | 2011-04-18 |
* | Fix unification of types of metavariables and error message for sort unificat... | msozeau | 2011-04-16 |
* | Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x". | herbelin | 2011-04-15 |
* | - Make typeclass transparency information directly available | msozeau | 2011-04-13 |
* | - Remove create_evar_defs | msozeau | 2011-04-13 |
* | - Improve unification (beta-reduction, and same heuristic as evarconv for red... | msozeau | 2011-04-13 |
* | Unify meta types with the right flags, add betaiotazeta reduction to unificat... | msozeau | 2011-04-13 |
* | Proper typing of metavariables, type errors were completely ignored before...... | msozeau | 2011-04-13 |
* | - Do not make constants with an assigned type polymorphic (wrong unfoldings). | msozeau | 2011-04-13 |
* | Catch NotArity exception and transform it into an anomaly in retyping. | msozeau | 2011-04-11 |
* | Applying and reworking Tom Prince's patch for test-suite/failure/universes2.v | herbelin | 2011-04-08 |
* | Replaced printing number of ill-typed branch by printing name of constructor | herbelin | 2011-04-08 |
* | A few extra combinators about rel_declaration/named_declaration + a bit of doc | herbelin | 2011-04-06 |
* | As remarked by Enrico, we'd better use eq_constr than structural equality | herbelin | 2011-03-31 |
* | - Remove useless grammar rule | msozeau | 2011-03-23 |
* | - Fix solve_simpl_eqn which was cheking instances types in the wrong environm... | msozeau | 2011-03-23 |
* | 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 |