aboutsummaryrefslogtreecommitdiff
path: root/tactics/rewrite.ml
AgeCommit message (Expand)Author
2015-02-16Fixing bug #3944.Pierre-Marie Pédrot
2015-02-14Fixing bug #4016.Pierre-Marie Pédrot
2015-01-24Tentative workaround for bug #3798.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2015-01-06Fix setoid rewrite.Arnaud Spiwack
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-02For compatibility purpose, when setoid_rewriting a hypothesis, beta-iotaPierre-Marie Pédrot
2014-12-01More invariants in the code of Rewrite.Pierre-Marie Pédrot
2014-11-30Set use_evars_eagerly_in_conv_on_closed_terms in rewrite_unif_flags too.Hugo Herbelin
2014-11-22Attempt to organize and document unification flags of setoid rewrite.Hugo Herbelin
2014-11-22In setoid_rewrite error messages:Hugo Herbelin
2014-11-22Fix resolve_morphism to build well-scoped terms in case some argumentsMatthieu Sozeau
2014-11-18Tentative rephrasing of error message for rewrite.Hugo Herbelin
2014-11-10Replugging hints in rewriting strategies.Pierre-Marie Pédrot
2014-11-08Follow up to experimental eager evar unification in bcba6d1bc9:Hugo Herbelin
2014-10-27Cleaning and documenting Clenv.make_evar_clausePierre-Marie Pédrot
2014-10-26Preventing potential evar leak in Rewrite.Pierre-Marie Pédrot
2014-10-24Change reduction_of_red_expr to return an e_reduction_function returningMatthieu Sozeau
2014-10-22Proofview: move more functions to the Unsafe module.Arnaud Spiwack
2014-10-22Proofview: split [V82] module into [Unsafe] and [V82].Arnaud Spiwack
2014-10-22Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Arnaud Spiwack
2014-10-21Removing dead code in Rewrite.Pierre-Marie Pédrot
2014-10-21Small invariants in Rewrite code.Pierre-Marie Pédrot
2014-10-21Fixing decompose_app_rel in Rewrite.Pierre-Marie Pédrot
2014-10-21Using new clausenv in rewrite.Pierre-Marie Pédrot
2014-10-16Proofview.Refine: remove the handle type, and simplify the API.Arnaud Spiwack
2014-10-09A version of convert_concl and convert_hyp in new proof engine.Hugo Herbelin
2014-10-07Splitting out of auto.ml a file hints.ml dedicated to hints so as toHugo Herbelin
2014-10-05Semantic fix of a refine in Rewrite.Pierre-Marie Pédrot
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _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-15A small pass of code cleaning and clenv removing in Rewrite.Pierre-Marie Pédrot
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-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-11Use an AST for strategy names.Matthieu Sozeau
2014-09-10A step towards better differentiating when w_unify is used for subtermHugo Herbelin
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
2014-09-05Fix parsing of "subterm(s)" strategy argument.Matthieu Sozeau
2014-09-04Typing.sort_of does not leak evarmaps anymore.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 15:55:19 +0000