| Age | Commit message (Expand) | Author |
|---|
| 2011-04-13 | Add [Polymorphic] flag for defs | msozeau |
| 2011-04-08 | Applying Tom Prince's patch for build_constant_by_tactic not able to | herbelin |
| 2011-03-18 | A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> seconds | letouzey |
| 2011-03-13 | - Add modulo_delta_types flag for unification to allow full | msozeau |
| 2011-03-11 | 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-10 | Forgot a use of evars_reset_evd in nf_evars, add an optional argument as | msozeau |
| 2011-03-08 | Fix declarations of [Add Setoid/Morphism...] in sections to not export | msozeau |
| 2011-03-05 | Fixing injection bug #2493 (regression introduced by fixing injection | herbelin |
| 2011-03-04 | - Allow to set a particular transparent_state for the local hint | msozeau |
| 2011-02-28 | - Allow rewriting under abitrary products, not just those in Prop. | msozeau |
| 2011-02-17 | - Use transparency information all the way through unification and | msozeau |
| 2011-02-14 | - Fix treatment of globality flag for typeclass instance hints (they | msozeau |
| 2011-02-11 | 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-10 | - 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-09 | One more fix for setoid_rewrite: completely reinterpret the given lemmas | msozeau |
| 2011-02-08 | Correct handling of existential variables when multiple different | msozeau |
| 2011-02-07 | Factorize code of rewrite to make way for a new implementation using the | msozeau |
| 2011-02-03 | Repair Class_tactics.split_evars, broken by r13717 (should fix #2481) | letouzey |
| 2011-01-31 | A fine-grain control of inlining at functor application via priority levels | letouzey |
| 2011-01-28 | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey |
| 2011-01-11 | Add [Typeclasses Debug] option that respects backtracking, solve | msozeau |
| 2010-12-27 | Rename the "raw" argument extension into "glob" | glondu |
| 2010-12-25 | ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPED | glondu |
| 2010-12-24 | More {raw => glob} changes for consistency | glondu |
| 2010-12-24 | tactics/eqdecide.ml4: avoid a useless argument in decideEquality | glondu |
| 2010-12-23 | Remove the two-argument variant of "decide equality" | glondu |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-12-23 | Change of nomenclature: rawconstr -> glob_constr | glondu |
| 2010-12-15 | Evar-related speed-up and clarifications in Class_tactics and Rewrite | letouzey |
| 2010-12-15 | Misc improvements about evar_map | letouzey |
| 2010-12-13 | Class_tactics: avoid an Evd.fold taking ages in contrib ProjectiveGeometry | letouzey |
| 2010-12-02 | Add tactic has_evar (#2433) | glondu |
| 2010-12-02 | Add tactic is_evar (Closes: #2433) | glondu |
| 2010-11-07 | Delayed the evar normalization in error messages to the last minute | herbelin |
| 2010-10-31 | 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 code cleaning in auto.ml (made code of make_exact_entry and | herbelin |
| 2010-10-27 | correction of bug #2414 (report of r 13586) | jforest |
| 2010-10-23 | Automatically translate hints of the form "c _ ... _" into "c". Besides | herbelin |
| 2010-10-04 | Two [Evd.fold] turned into [Evd.fold_undefined]. | aspiwack |
| 2010-09-30 | Simplify tactic(_)-bound arguments in TACTIC EXTEND rules | glondu |
| 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-27 | Fix bug in implementation of setoid rewriting under cases and | msozeau |
| 2010-09-24 | Solving bug #2212 (unification under tuples now not allowed for | herbelin |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
