| Commit message (Expand) | Author | Age |
* | This is exactly the structure needed to handle controlling printing | herbelin | 2011-07-16 |
* | Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml | letouzey | 2011-07-04 |
* | Cleaning debugging printer relative to new proof engine. In | herbelin | 2011-06-21 |
* | Fixing two typos introduced in r14217 and r14223 | herbelin | 2011-06-20 |
* | Ensured that the transparency state is used when flag betaiota is on for apply. | herbelin | 2011-06-19 |
* | Generalizing flag use_evars_pattern_unification into a flag | herbelin | 2011-06-18 |
* | Activating flags betaiota by default for apply | herbelin | 2011-06-18 |
* | The ad hoc version for first-order unification at toplevel of "?n args | herbelin | 2011-06-18 |
* | Added full pattern-unification on Meta for tactic unification. | herbelin | 2011-06-13 |
* | Added a flag to restrict conversion in tactic unification on the | herbelin | 2011-06-13 |
* | Oups, typo in previous commit | herbelin | 2011-06-12 |
* | Removed what looks like a (very old) useless f.o. unification pass | herbelin | 2011-06-12 |
* | Added a new flag for freezing evars in tactic unification. Used this | herbelin | 2011-06-12 |
* | Moved allow_K to a unification flag | herbelin | 2011-06-10 |
* | 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 |
* | Applying Enrico Tassi's patch for giving priority to delta over eta in | herbelin | 2011-05-24 |
* | Failing instead of switching to the coercion mechanism when VMcast | herbelin | 2011-05-15 |
* | A better procedure for checking presence of undefined evars. | aspiwack | 2011-05-13 |
* | Fix merge, Cumul moved to CUMUL | msozeau | 2011-05-05 |
* | Merge branch 'subclasses' into coq-trunk | msozeau | 2011-05-05 |
* | First phase removing obsolete support for eta up to conversion in | herbelin | 2011-05-04 |
* | Fixing bug in printing let-in binders in fix/cofix | herbelin | 2011-04-24 |
* | 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 |