aboutsummaryrefslogtreecommitdiff
path: root/tactics/rewrite.ml
AgeCommit message (Expand)Author
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
2014-09-03Putting back normalized goals when entering them.Pierre-Marie Pédrot
2014-08-27Protect against "it's unifiable, if you solve some unsolvable constraints" be...Matthieu Sozeau
2014-08-22Move UnsatisfiableConstraints to a pretype error.Matthieu Sozeau
2014-08-21Removing a Goal.sensitive in Rewrite.Pierre-Marie Pédrot
2014-08-21Removing a use of tclSENSITIVE in Rewrite.Pierre-Marie Pédrot
2014-08-21Removing a use of tclSENSITIVE in Rewrite.Pierre-Marie Pédrot
2014-08-21Removing a use of tclSENSITIVE in Rewrite.Pierre-Marie Pédrot
2014-08-18Improving error message when applying rewrite to an expression which is not a...Hugo Herbelin
2014-08-18Slight simplification of naming of tactics in equality.ml (hopefully).Hugo Herbelin
2014-08-18A reorganization of the "assert" tactics (hopefully uniform namingHugo Herbelin
2014-08-18Reorganization of tactics:Hugo Herbelin
2014-08-18Refine patch for behavior of unify_to_subterm to allow backtracking onMatthieu Sozeau
2014-08-14Remove confusing behavior of unify_with_subterm that could fail withMatthieu Sozeau
2014-07-14Redo PMP's patch to rewriting to make it purely functional using state passing.Matthieu Sozeau
2014-07-10check_for_interrupt: better (but slower) in threading modeEnrico Tassi
2014-07-02In setoid_rewrite, force resolution of the contraints generated by rewriting ...Matthieu Sozeau
2014-06-27Add an init_setoid check in rewrite to avoid trying to get undefined references.Matthieu Sozeau
2014-06-25In rewrite, wrong computation of the sort of the term to be rewritten inMatthieu Sozeau
2014-06-23Fix semantics of change p with c to typecheck c at each specific occurrence o...Matthieu Sozeau
2014-06-20Allow more relaxed conversion between the types of the two terms of a rewriteMatthieu Sozeau
2014-06-19- Fix bug in unification, not only named metas are turned into evars (e.g. in...Matthieu Sozeau
2014-06-18Proofs now take and return an evar_universe_context, simplifying interfacesMatthieu Sozeau
2014-06-17Removing dead code.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 13:59:53 +0000