| Commit message (Expand) | Author | Age |
|---|
| * | A few comments and a dev file to summarize issues with unification |  herbelin | 2011-06-13 |
| * | Added a flag to restrict conversion in tactic unification on the | herbelin | 2011-06-13 |
| * | 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 |
| * | Fixing another bug with "_" intro pattern. | herbelin | 2011-06-10 |
| * | Fixing the "buggy" first_name and prepare multi-induction. | herbelin | 2011-06-10 |
| * | Made use of "_" in repeated use of intros_patterns work (with | herbelin | 2011-06-10 |
| * | Integrating onLastHypId into intro so that we can get the introduction | herbelin | 2011-06-10 |
| * | Fix bug #2335, fail if the search for reflexivity/symmetry/transitivity proof... |  msozeau | 2011-06-07 |
| * | Fixing discriminate for identity. | herbelin | 2011-05-26 |
| * | Class_tactics: Pervasives.(=) don't work for named_context_val (fix ATBR) |  letouzey | 2011-05-17 |
| * | More work on error handling | letouzey | 2011-05-17 |
| * | Merge branch 'subclasses' into coq-trunk | msozeau | 2011-05-05 |
| * | Revert r14078 "Partial backtrack on the support for open terms in destruct/in... |  gmelquio | 2011-04-28 |
| * | Partial backtrack on the support for open terms in destruct/induction: | gmelquio | 2011-04-28 |
| * | Fixing commit r14061 (changes in file tactics.ml were mistakenly committed). | herbelin | 2011-04-26 |
| * | Fixing and completing interpretation of let's in notations for iterated binders. | herbelin | 2011-04-25 |
| * | Fixed a bug of destruct which was sometimes forgetting local definitions behi... | herbelin | 2011-04-24 |
| * | Don't force progress on instance applications, there is always progress when ... | msozeau | 2011-04-20 |
| * | This is used in the rippling plugin. This also allows fixing bug #2188. | msozeau | 2011-04-20 |
| * | Add a flag to control betaiota reduction during unification to maintain backw... | msozeau | 2011-04-18 |
| * | More informative anomaly. | herbelin | 2011-04-14 |
| * | Revert "Add [Polymorphic] flag for defs" | msozeau | 2011-04-13 |
| * | Put dependent subgoals first so as to allow backtracking on them, might chang... | msozeau | 2011-04-13 |
| * | - 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 |
| * | - Do not make constants with an assigned type polymorphic (wrong unfoldings). | msozeau | 2011-04-13 |
| * | Add [Polymorphic] flag for defs | msozeau | 2011-04-13 |
| * | Applying Tom Prince's patch for build_constant_by_tactic not able to | herbelin | 2011-04-08 |
| * | A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> seconds | letouzey | 2011-03-18 |
| * | - 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 |
| * | - 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 |
| * | Fix declarations of [Add Setoid/Morphism...] in sections to not export | msozeau | 2011-03-08 |
| * | Fixing injection bug #2493 (regression introduced by fixing injection | herbelin | 2011-03-05 |
| * | - Allow to set a particular transparent_state for the local hint | msozeau | 2011-03-04 |
| * | - Allow rewriting under abitrary products, not just those in Prop. | msozeau | 2011-02-28 |
| * | - 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 |
| * | Try to clarify a bit Class_tactics (comments, refactoring,...) | letouzey | 2011-02-11 |
| * | An generic imperative union-find, used for deps of evars in Class_tactics | letouzey | 2011-02-11 |
| * | Change Evd.fold to a faster version that simply removes unneeded evars. | msozeau | 2011-02-11 |
| * | - proper printing of setoid_rewrite tactic applications | msozeau | 2011-02-10 |
| * | Rename subst_raw_with_bindings to subst_glob_with_bindings and export | msozeau | 2011-02-10 |
| * | One more fix for setoid_rewrite: completely reinterpret the given lemmas | msozeau | 2011-02-09 |
| * | Correct handling of existential variables when multiple different | msozeau | 2011-02-08 |
| * | Factorize code of rewrite to make way for a new implementation using the | msozeau | 2011-02-07 |
| * | Repair Class_tactics.split_evars, broken by r13717 (should fix #2481) | letouzey | 2011-02-03 |
herbelin
msozeau
letouzey
gmelquio