aboutsummaryrefslogtreecommitdiff
path: root/tactics/rewrite.ml
AgeCommit message (Expand)Author
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
2014-06-11Fix bug #3291, stack overflow in rewrite.Matthieu Sozeau
2014-06-11Fix bug #3289Matthieu Sozeau
2014-06-11In generalized rewrite, avoid retyping completely and constantly the conclusi...Matthieu Sozeau
2014-06-08Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofPierre-Marie Pédrot
2014-06-08Enforce a correct exception handling in declaration_hooksEnrico Tassi
2014-06-04Collecting in Namegen those conventional default names that are used in diffe...Hugo Herbelin
2014-05-31Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").Hugo Herbelin
2014-05-27Removing a tclSENSITIVE from rewrite.Pierre-Marie Pédrot
2014-05-09Update and start testing rewrite-in-type code.Matthieu Sozeau
2014-05-08Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic."Hugo Herbelin
2014-05-08Avoid "revert" to retype-check the goal, and move it to a "new" tactic.Hugo Herbelin
2014-05-06- Fix treatment of global universe constraints which should be passed alongMatthieu Sozeau
2014-05-06- Fix arity handling in retyping (de Bruijn bug!)Matthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-22 07:52:56 +0000