aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Merge branch 'subclasses' into coq-trunkGravatar msozeau2011-05-05
* Revert r14078 "Partial backtrack on the support for open terms in destruct/in...Gravatar gmelquio2011-04-28
* Partial backtrack on the support for open terms in destruct/induction:Gravatar gmelquio2011-04-28
* Fixing commit r14061 (changes in file tactics.ml were mistakenly committed).Gravatar herbelin2011-04-26
* Fixing and completing interpretation of let's in notations for iterated binders.Gravatar herbelin2011-04-25
* Fixed a bug of destruct which was sometimes forgetting local definitions behi...Gravatar herbelin2011-04-24
* Don't force progress on instance applications, there is always progress when ...Gravatar msozeau2011-04-20
* This is used in the rippling plugin. This also allows fixing bug #2188.Gravatar msozeau2011-04-20
* Add a flag to control betaiota reduction during unification to maintain backw...Gravatar msozeau2011-04-18
* More informative anomaly.Gravatar herbelin2011-04-14
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
* Put dependent subgoals first so as to allow backtracking on them, might chang...Gravatar msozeau2011-04-13
* - Make typeclass transparency information directly availableGravatar msozeau2011-04-13
* - Remove create_evar_defsGravatar msozeau2011-04-13
* - Improve unification (beta-reduction, and same heuristic as evarconv for red...Gravatar msozeau2011-04-13
* - Do not make constants with an assigned type polymorphic (wrong unfoldings).Gravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* Applying Tom Prince's patch for build_constant_by_tactic not able toGravatar herbelin2011-04-08
* A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsGravatar letouzey2011-03-18
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* Keep information on which fields are subclasses in class declarations,Gravatar msozeau2011-03-11
* - Better error messages taking unif. constraints into account.Gravatar msozeau2011-03-11
* Forgot a use of evars_reset_evd in nf_evars, add an optional argument asGravatar msozeau2011-03-10
* Fix declarations of [Add Setoid/Morphism...] in sections to not exportGravatar msozeau2011-03-08
* Fixing injection bug #2493 (regression introduced by fixing injectionGravatar herbelin2011-03-05
* - Allow to set a particular transparent_state for the local hintGravatar msozeau2011-03-04
* - Allow rewriting under abitrary products, not just those in Prop.Gravatar msozeau2011-02-28
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
* - Fix treatment of globality flag for typeclass instance hints (theyGravatar msozeau2011-02-14
* Try to clarify a bit Class_tactics (comments, refactoring,...)Gravatar letouzey2011-02-11
* An generic imperative union-find, used for deps of evars in Class_tacticsGravatar letouzey2011-02-11
* Change Evd.fold to a faster version that simply removes unneeded evars.Gravatar msozeau2011-02-11
* - proper printing of setoid_rewrite tactic applicationsGravatar msozeau2011-02-10
* Rename subst_raw_with_bindings to subst_glob_with_bindings and exportGravatar msozeau2011-02-10
* One more fix for setoid_rewrite: completely reinterpret the given lemmasGravatar msozeau2011-02-09
* Correct handling of existential variables when multiple differentGravatar msozeau2011-02-08
* Factorize code of rewrite to make way for a new implementation using theGravatar msozeau2011-02-07
* Repair Class_tactics.split_evars, broken by r13717 (should fix #2481)Gravatar letouzey2011-02-03
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* Add [Typeclasses Debug] option that respects backtracking, solveGravatar msozeau2011-01-11
* Rename the "raw" argument extension into "glob"Gravatar glondu2010-12-27
* ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPEDGravatar glondu2010-12-25
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* tactics/eqdecide.ml4: avoid a useless argument in decideEqualityGravatar glondu2010-12-24
* Remove the two-argument variant of "decide equality"Gravatar glondu2010-12-23
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Evar-related speed-up and clarifications in Class_tactics and RewriteGravatar letouzey2010-12-15
* Misc improvements about evar_mapGravatar letouzey2010-12-15