aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2014-09-24Rename eq_constr functions in Evd to not break backward compatibilityMatthieu Sozeau
2014-09-24Make eq_pattern_test/eq_test work up to the equivalence of primitiveMatthieu Sozeau
2014-09-24Using an or_var rather than the hack with loc for coding a pure identHugo Herbelin
2014-09-24Added support for interpreting hyp lists in tactic notations.Hugo Herbelin
2014-09-23ATBR can't compile without the fix, as it uses setoid_rewrite to rewriteMatthieu Sozeau
2014-09-23Fix bug in setoid_rewrite introduced by PMP's commits, which was creatingMatthieu Sozeau
2014-09-21Rewrite.apply_lemma is written in state passing style.Pierre-Marie Pédrot
2014-09-21More invariants in the code of Refine.Pierre-Marie Pédrot
2014-09-21Removing a nonsensical Errors.push.Pierre-Marie Pédrot
2014-09-18Fixing strange evarmap leak in goals.Pierre-Marie Pédrot
2014-09-17Be more conservative and keep the use of eq_constr in pretyping/ functions.Matthieu Sozeau
2014-09-17Fix bug #3593, making constr_eq and progress work up toMatthieu Sozeau
2014-09-17Fix bug #3633 properly, by delaying the interpetation of constrs inMatthieu Sozeau
2014-09-17Revert specific syntax for primitive projections, avoiding uglyMatthieu Sozeau
2014-09-15Add a "Hint Mode ref (+ | -)*" hint for setting a global modeMatthieu Sozeau
2014-09-15Fix timing of evar-normalisation of goals in [Ftactic.nf_enter].Arnaud Spiwack
2014-09-15Ltac names in binders: some Ltac values can be seen both as terms and identif...Arnaud Spiwack
2014-09-15A small pass of code cleaning and clenv removing in Rewrite.Pierre-Marie Pédrot
2014-09-15Avoid backtracking in typeclass search if a solution for a closedMatthieu Sozeau
2014-09-15Rework typeclass resolution and control of backtracking.Matthieu Sozeau
2014-09-15Removing one Evd.merge in Rewrite.Pierre-Marie Pédrot
2014-09-15More invariants in Rewrite unification.Pierre-Marie Pédrot
2014-09-15The unifying functions of Rewrite uses the return types of strategies.Pierre-Marie Pédrot
2014-09-15Splitting the uses of the unification function according to the status ofPierre-Marie Pédrot
2014-09-14Rewrite.apply_strategy uses the same return type as strategies.Pierre-Marie Pédrot
2014-09-14Proper type for rewrite strategy results.Pierre-Marie Pédrot
2014-09-13Retroknowledge arguments are made VERNAC ARGUMENTS.Pierre-Marie Pédrot
2014-09-13Fixing injection bug #3616 on sigma-types.Hugo Herbelin
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-09-12Commit 682aa67cc80 about enforcing that apply does not create newHugo Herbelin
2014-09-11Oopps.. fixed the .ml not the .ml4Matthieu Sozeau
2014-09-11Use an AST for strategy names.Matthieu Sozeau
2014-09-11Add a flag for restricting resolution of typeclasses toMatthieu Sozeau
2014-09-11Keeping a sub-optimal behavior of intros_possibly_replacing for compatibility...Hugo Herbelin
2014-09-11Other bugs with "inversion as" (collision between user-provided names and gen...Hugo Herbelin
2014-09-10A step towards better differentiating when w_unify is used for subtermHugo Herbelin
2014-09-10Fixing localisation of tactic errors (my mistake in himsg.ml essentially).Hugo Herbelin
2014-09-10More small bugs in intros_replacing.Hugo Herbelin
2014-09-10Fixing inversion after having fixed intros_replacingHugo Herbelin
2014-09-09Displaying genarg tag in idtac.Pierre-Marie Pédrot
2014-09-08Removing antiquotations in Tauto.Pierre-Marie Pédrot
2014-09-08Removing the XML plugin.Pierre-Marie Pédrot
2014-09-08Display number of available goals in "incorrect number of goals" error message.Arnaud Spiwack
2014-09-08Fix [induction] wrt inductive records and non-recursive variants.Arnaud Spiwack
2014-09-08Rename [extract_ltac_uconstr_values] to [extract_ltac_constr_context].Arnaud Spiwack
2014-09-08The [constr:(…)] Ltac construction now shares the same context as [uconstr:...Arnaud Spiwack
2014-09-08Add a tactic [revgoals] to reverse the list of focused goals.Arnaud Spiwack
2014-09-07A better check that an "as" clause has been given to inversion, soHugo Herbelin
2014-09-07Fixing a bug in intros_replacing which was causing inversion notHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-19 10:09:59 +0000