aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2011-04-13- Do not make constants with an assigned type polymorphic (wrong unfoldings).msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-04-08Applying Tom Prince's patch for build_constant_by_tactic not able toherbelin
2011-03-18A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsletouzey
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
2011-03-11Keep information on which fields are subclasses in class declarations,msozeau
2011-03-11- Better error messages taking unif. constraints into account.msozeau
2011-03-10Forgot a use of evars_reset_evd in nf_evars, add an optional argument asmsozeau
2011-03-08Fix declarations of [Add Setoid/Morphism...] in sections to not exportmsozeau
2011-03-05Fixing injection bug #2493 (regression introduced by fixing injectionherbelin
2011-03-04- Allow to set a particular transparent_state for the local hintmsozeau
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 andmsozeau
2011-02-14- Fix treatment of globality flag for typeclass instance hints (theymsozeau
2011-02-11Try to clarify a bit Class_tactics (comments, refactoring,...)letouzey
2011-02-11An generic imperative union-find, used for deps of evars in Class_tacticsletouzey
2011-02-11Change Evd.fold to a faster version that simply removes unneeded evars.msozeau
2011-02-10- proper printing of setoid_rewrite tactic applicationsmsozeau
2011-02-10Rename subst_raw_with_bindings to subst_glob_with_bindings and exportmsozeau
2011-02-09One more fix for setoid_rewrite: completely reinterpret the given lemmasmsozeau
2011-02-08Correct handling of existential variables when multiple differentmsozeau
2011-02-07Factorize code of rewrite to make way for a new implementation using themsozeau
2011-02-03Repair Class_tactics.split_evars, broken by r13717 (should fix #2481)letouzey
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2011-01-11Add [Typeclasses Debug] option that respects backtracking, solvemsozeau
2010-12-27Rename the "raw" argument extension into "glob"glondu
2010-12-25ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPEDglondu
2010-12-24More {raw => glob} changes for consistencyglondu
2010-12-24tactics/eqdecide.ml4: avoid a useless argument in decideEqualityglondu
2010-12-23Remove the two-argument variant of "decide equality"glondu
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-12-15Evar-related speed-up and clarifications in Class_tactics and Rewriteletouzey
2010-12-15Misc improvements about evar_mapletouzey
2010-12-13Class_tactics: avoid an Evd.fold taking ages in contrib ProjectiveGeometryletouzey
2010-12-02Add tactic has_evar (#2433)glondu
2010-12-02Add tactic is_evar (Closes: #2433)glondu
2010-11-07Delayed the evar normalization in error messages to the last minuteherbelin
2010-10-31An experimental support for open constrs in hints and in "using"herbelin
2010-10-31Cleaning the use of parentheses around evd and evdref (cosmetic commit).herbelin
2010-10-31Slight code cleaning in auto.ml (made code of make_exact_entry andherbelin
2010-10-27correction of bug #2414 (report of r 13586)jforest
2010-10-23Automatically translate hints of the form "c _ ... _" into "c". Besidesherbelin
2010-10-04Two [Evd.fold] turned into [Evd.fold_undefined].aspiwack
2010-09-30Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesglondu
2010-09-28Remove some occurrences of "open Termops"glondu
2010-09-28Remove "init" label from Termops.it_mk* specialized functionsglondu
2010-09-27Fix bug in implementation of setoid rewriting under cases andmsozeau
2010-09-24Solving bug #2212 (unification under tuples now not allowed forherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 22:04:22 +0000