| Commit message (Expand) | Author | Age |
* | 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 |
* | A fine-grain control of inlining at functor application via priority levels | letouzey | 2011-01-31 |
* | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey | 2011-01-28 |
* | Add [Typeclasses Debug] option that respects backtracking, solve | msozeau | 2011-01-11 |
* | Rename the "raw" argument extension into "glob" | glondu | 2010-12-27 |
* | ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPED | glondu | 2010-12-25 |
* | More {raw => glob} changes for consistency | glondu | 2010-12-24 |
* | tactics/eqdecide.ml4: avoid a useless argument in decideEquality | glondu | 2010-12-24 |
* | 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-23 |
* | Evar-related speed-up and clarifications in Class_tactics and Rewrite | letouzey | 2010-12-15 |
* | Misc improvements about evar_map | letouzey | 2010-12-15 |
* | Class_tactics: avoid an Evd.fold taking ages in contrib ProjectiveGeometry | letouzey | 2010-12-13 |
* | Add tactic has_evar (#2433) | glondu | 2010-12-02 |
* | Add tactic is_evar (Closes: #2433) | glondu | 2010-12-02 |
* | 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 code cleaning in auto.ml (made code of make_exact_entry and | herbelin | 2010-10-31 |
* | correction of bug #2414 (report of r 13586) | jforest | 2010-10-27 |
* | Automatically translate hints of the form "c _ ... _" into "c". Besides | herbelin | 2010-10-23 |
* | Two [Evd.fold] turned into [Evd.fold_undefined]. | aspiwack | 2010-10-04 |
* | Simplify tactic(_)-bound arguments in TACTIC EXTEND rules | glondu | 2010-09-30 |
* | Remove some occurrences of "open Termops" | glondu | 2010-09-28 |
* | Remove "init" label from Termops.it_mk* specialized functions | glondu | 2010-09-28 |
* | Fix bug in implementation of setoid rewriting under cases and | msozeau | 2010-09-27 |
* | Solving bug #2212 (unification under tuples now not allowed for | herbelin | 2010-09-24 |
* | 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 |
* | Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't we | herbelin | 2010-09-19 |
* | Reverting partial fix for #2335 committed by mistake in r13435. Sorry. | herbelin | 2010-09-19 |
* | Patch solving the bug but leaving open design choices | herbelin | 2010-09-19 |
* | Fixed a problem introduced in r12607 after pattern_of_constr served | herbelin | 2010-09-17 |
* | In the computation of missing arguments for apply, accept that the | herbelin | 2010-09-17 |
* | Fix unescaped end-of-lines (OCaml warning 29) | glondu | 2010-09-13 |
* | Improving a few error messages in Ltac interpretation | herbelin | 2010-09-11 |