aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
2014-09-07Fixing "simple inversion as" (bug #2164).Hugo Herbelin
2014-09-07Dead code in inv.ml.Hugo Herbelin
2014-09-06Inlining code in Tacinterp that was only used once.Pierre-Marie Pédrot
2014-09-06Code simplification in Tacinterp.Pierre-Marie Pédrot
2014-09-06Proper interpretation function for tauto.Pierre-Marie Pédrot
2014-09-06Adding a way to inject tactic closures in interpretation values.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-19 07:50:45 +0000